A classification of symbolic transition systems

ABSTRACT

We define five increasingly comprehensive classes of infinite-state systems, called STS1--STS5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.STS1 These are the systems with finite bisimilarity quotients. They can be analyzed symbolically by iteratively applying predecessor and Boolean operations on state sets, starting from a finite number of observable state sets. Any such iteration is guaranteed to terminate in that only a finite number of state sets can be generated. This enables model checking of the μ-calculus.STS2 These are the systems with finite similarity quotients. They can be analyzed symbolically by iterating the predecessor and positive Boolean operations. This enables model checking of the existential and universal fragments of the μ-calculus.STS3 These are the systems with finite trace-equivalence quotients. They can be analyzed symbolically by iterating the predecessor operation and a restricted form of positive Boolean operations (intersection is restricted to intersection with observables). This enables model checking of all ω-regular properties, including linear temporal logic.STS4 These are the systems with finite distance-equivalence quotients (two states are equivalent if for every distance d, the same observables can be reached in d transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new state sets are generated. This enables model checking of the existential conjunction-free and universal disjunction-free fragments of the μ-calculus.STS5 These are the systems with finite bounded-reachability quotients (two states are equivalent if for every distance d, the same observables can be reached in d or fewer transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new states are encountered (this is a weaker termination condition than above). This enables model checking of reachability properties.

REFERENCES

• 1: Parosh Aziz Abdulla , Bengt Jonsson, Verifying Networks of Timed Processes (Extended Abstract), Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.298-312, March 28-April 04, 1998
• 2: P. A. Abdulla , K. Cerans , B. Jonsson , Yih-Kuen Tsay, General decidability theorems for infinite-state systems, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.313, July 27-30, 1996
• 3: R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995 [doi>10.1016/0304-3975(94)00202-T]
• 4: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 5: Alur, R. and Henzinger, T. 1998. Computer-Aided Verification: An Introduction to Model Building and Model Checking for Concurrent Systems. Draft.
• 6: Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996 [doi>10.1109/32.489079]
• 7: Berman, L. 1980. The complexity of logical theories. Theoret. Comput. Sci. 11, 71--77.
• 8: G. Bhat , R. Cleaveland, Efficient model checking via the equational /spl mu/-calculus, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.304, July 27-30, 1996
• 9: Ahmed Bouajjani , Jean-Claude Fernandez , Nicolas Halbwachs, Minimal Model Generation, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.197-203, June 18-21, 1990
• 10: M. C. Browne , E. M. Clarke , O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science, v.59 n.1-2, p.115-131, July 1988 [doi>10.1016/0304-3975(88)90098-9]
• 11: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 12: Doron Bustan , Orna Grumberg, Simulation-based minimization, ACM Transactions on Computational Logic (TOCL), v.4 n.2, p.181-206, April 2003 [doi>10.1145/635499.635502]
• 13: Edmund M. Clarke , Orna Grumberg , David E. Long, Verification Tools for Finite-State Concurrent Systems, A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, p.124-175, June 01-04, 1993
• 14: Rance Cleaveland , Marion Klein , Bernhard Steffen, Faster Model Checking for the Modal Mu-Calculus, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.410-422, June 29-July 01, 1992
• 15: Cooper, D. C. 1972. Theorem proving in arithmetic without multiplication. Mach. Intel. 7, 91--100.
• 16: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 17: Mads Dam, CTL and ECTL as fragments of the modal &mgr;-calculus, Theoretical Computer Science, v.126 n.1, p.77-96, April 11, 1994 [doi>10.1016/0304-3975(94)90269-0]
• 18: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 19: E. Allen Emerson , Charanjit S. Jutla , A. Prasad Sistla, On Model-Checking for Fragments of µ-Calculus, Proceedings of the 5th International Conference on Computer Aided Verification, p.385-396, June 28-July 01, 1993
• 20: E. Allen Emerson , Charanjit S. Jutla , A. Prasad Sistla, On model checking for the &mgr;-calculus and its fragments, Theoretical Computer Science, v.258 n.1-2, p.491-522, May 2001 [doi>10.1016/S0304-3975(00)00034-7]
• 21: Emerson, E. and Lei, C. 1986. Efficient model checking in fragments of the propositional μ-calculus. In Proceedings of the 1st Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 267--278.
• 22: Finkel, A. and Schnoebelen, P. 1998. Well-structured Transition Systems Everywhere. Tech. Rep. LSV-98-4, Laboratoire Spécification et Vérification, ENS de Cachan, France.
• 23: M. R. Henzinger , T. A. Henzinger , P. W. Kopke, Computing simulations on finite and infinite graphs, Proceedings of the 36th Annual Symposium on Foundations of Computer Science (FOCS'95), p.453, October 23-25, 1995
• 24: Thomas A. Henzinger, Hybrid Automata with Finite Bisimulatioins, Proceedings of the 22nd International Colloquium on Automata, Languages and Programming, p.324-335, July 10-14, 1995
• 25: T. A. Henzinger, The theory of hybrid automata, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.278, July 27-30, 1996
• 26: T. A. Henzinger , Pei-Hsin Ho , H. Wong-Toi, HYTECH: the next generation, Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS '95), p.56, December 05-07, 1995
• 27: Thomas A. Henzinger , Peter W. Kopke, State Equivalences for Rectangular Hybrid Automata, Proceedings of the 7th International Conference on Concurrency Theory, p.530-545, August 26-29, 1996
• 28: Thomas A. Henzinger , Peter W. Kopke , Anuj Puri , Pravin Varaiya, What's decidable about hybrid automata?, Journal of Computer and System Sciences, v.57 n.1, p.94-124, Aug. 1998 [doi>10.1006/jcss.1998.1581]
• 29: Thomas A. Henzinger , Rupak Majumdar, Symbolic Model Checking for Rectangular Hybrid Systems, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.142-156, March 25-April 02, 2000
• 30: Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Symbolic model checking for real-time systems, Information and Computation, v.111 n.2, p.193-244, June 1994 [doi>10.1006/inco.1994.1045]
• 31: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 32: David Janin , Igor Walukiewicz, On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic, Proceedings of the 7th International Conference on Concurrency Theory, p.263-277, August 26-29, 1996
• 33: Paris C. Kanellakis , Scott A. Smolka, CCS expressions finite state processes, and three problems of equivalence, Information and Computation, v.86 n.1, p.43-68, May 1990 [doi>10.1016/0890-5401(90)90025-D]
• 34: Kozen, D. 1983. Results on the propositional μ-calculus. Theoret. Comput. Sci. 27, 333--354.
• 35: Leslie Lamport, A new solution of Dijkstra's concurrent programming problem, Communications of the ACM, v.17 n.8, p.453-455, Aug. 1974 [doi>10.1145/361082.361093]
• 36: C. Loiseaux , S. Graf , J. Sifakis , A. Bouajjani , S. Bensalem, Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, v.6 n.1, p.11-44, Jan. 1995 [doi>10.1007/BF01384313]
• 37: Milner, R. 1971. An algebraic definition of simulation between programs. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence. The British Computer Society, 481--489.
• 38: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 39: van Glabbeek, R. 1990. Comparative Concurrency Semantics and Refinement of Actions. Ph.D. Thesis, Vrije Universiteit te Amsterdam, The Netherlands.
• 40: Wolper, P. 1983. Temporal logic can be more expressive. Inf. Cont. 56, 72--99.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Verification

Keywords:
Model checking, hybrid automata, infinite-state model checking, state equivalences, symbolic algorithms, temporal logics