Model checking real-time properties of symmetric systems

DOI10.1007/BFB0055792MaRDI QIDQ4218117zbMATH OpenFDO

Authors Richard Trefler, E. Allen Emerson

Publication date 24 May 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0055792

zbMATH Keywords

finite state systemmodel checkingreal-time mu-calculussymmetric reactive systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Effective algorithms for model checking quantitative properties of symmetric reactive systems in the framework of a (discrete) Real-Time Mu-calculus (RTL\(\mu\)) are developed. To reduce the number of states of a given finite state system \(M\), two quotient structures, \(M^\ast\) (transitions between states are labeled with permutations indicating how the meaning of all coordinates shift) and \(\widehat{M}\) (transitions between states are labeled with permutations indicating how the meaning of individual coordinates shift), are introduced. An \(O(| \widehat{M}| | f| n)\) algorithm, which actually operates on \(M^\ast\), for evaluating Indexed RTL\(\mu\) formulae of alternation depth 1 over \(\widehat{M}\) is given. For the entire collection see [Zbl 0895.00049].

Recommendations

• Symbolic model checking for real-time systems
• scientific article; zbMATH DE number 1796126
• Model-checking for real-time systems
• Model-checking for probabilistic real-time systems

Cited in

(4)

• Employing symmetry reductions in model checking
• Checking extended CTL properties using guarded quotient structures
• Model and program repair via group actions
• Model and program repair via group actions and structure unwinding

This page was built for publication: Model checking real-time properties of symmetric systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4218117)