University of Leicester
Browse
- No file added yet -

Bridging the gap between fair simulation and trace inclusion

Download (455.79 kB)
journal contribution
posted on 2012-03-26, 15:07 authored by Yonit Kesten, Nir Piterman, Amir Pnueli
The paper considers the problem of checking abstraction between two finite-state fair discrete systems. In automata-theoretic terms this is trace inclusion between two nondeterministic Streett automata. We propose to reduce this problem to an algorithm for checking fair simulation between two generalized Büchi automata. For solving this question we present a new triply nested μ-calculus formula which can be implemented by symbolic methods. We then show that every trace inclusion of this type can be solved by fair simulation, provided we augment the concrete system (the contained automaton) by an appropriate ‘non-constraining’ automaton. This establishes that fair simulation offers a complete method for checking trace inclusion for finite-state systems. We illustrate the feasibility of the approach by algorithmically checking abstraction between finite state systems whose abstraction could only be verified by deductive methods up to now.

History

Citation

Information and Computation, 2005, 200 (1), pp. 35-61.

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Version

  • AM (Accepted Manuscript)

Published in

Information and Computation

Publisher

Elsevier

issn

0890-5401

Copyright date

2005

Available date

2012-03-26

Publisher version

http://www.sciencedirect.com/science/article/pii/S0890540105000234

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC