TY - GEN
T1 - Local model checking for real-time systems
T2 - 7th International Conference on Computer Aided Verification, CAV 1995
AU - Sokolsky, Oleg V.
AU - Smolka, Scott A.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1995.
PY - 1995
Y1 - 1995
N2 - We present a local algorithm for model checking in a real-time extension of the modal mu-calculus. As such, the whole state space of the real-time system under investigation need not be explored, but rather only that portion necessary to determine the truthhood of the logical formula. To the best of our knowledge, this is the first local algorithm for the verification of real-time systems to appear in the literature. Like most algorithms dealing with real-time systems, we work with a finite quotient of the inherently infinite state space. For maximal efficiency, we obtain, on-the-fly, a quotient that is as coarse at possible in the following sense: refinements of the quotient are carried out only when necessary to satisfy clock constraints appearing in the logical formula or timed automaton used to represent the system under investigation. In this sense, our data structures are optimal with respect to the given formula and automaton.
AB - We present a local algorithm for model checking in a real-time extension of the modal mu-calculus. As such, the whole state space of the real-time system under investigation need not be explored, but rather only that portion necessary to determine the truthhood of the logical formula. To the best of our knowledge, this is the first local algorithm for the verification of real-time systems to appear in the literature. Like most algorithms dealing with real-time systems, we work with a finite quotient of the inherently infinite state space. For maximal efficiency, we obtain, on-the-fly, a quotient that is as coarse at possible in the following sense: refinements of the quotient are carried out only when necessary to satisfy clock constraints appearing in the logical formula or timed automaton used to represent the system under investigation. In this sense, our data structures are optimal with respect to the given formula and automaton.
UR - https://www.scopus.com/pages/publications/84947941425
U2 - 10.1007/3-540-60045-0_52
DO - 10.1007/3-540-60045-0_52
M3 - Conference contribution
AN - SCOPUS:84947941425
SN - 9783540600459
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 211
EP - 224
BT - Computer Aided Verification - 7th International Conference, CAV 1995, Proceedings
A2 - Wolper, Pierre
PB - Springer Verlag
Y2 - 3 July 1995 through 5 July 1995
ER -