Abstract
We build on the established work on modal transition systems and probabilistic specifications to sketch a framework in which system description, abstraction, and finite-state model checking all have a uniform presentation across various levels of qualitative and quantitative views together with mediating abstraction and concretization maps. We prove safety results for abstractions within and across such views for the entire modal mu-calculus and show that such abstractions allow for some compositional reasoning with respect to a uniform family of process algebras à la CCS.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
C. Baier. Polynomial Time Algorithms for Testing Probabilistic Bisimulation and Simulation. In Proceedings of CAV’96, number 1102 in Lecture Notes in Computer Science, pages 38–49. Springer Verlag, 1996. 370
C. Baier, M. Kwiatkowska, and G. Norman. Computing probability bounds for linear time formulas over concurrent probabilistic systems. Electronic Notes in Theoretical Computer Science, 21:19 pages, 1999. 378
E. M. Clarke and E. M. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In D. Kozen, editor, Proc. Logic of Programs, volume 131 of LNCS. Springer Verlag, 1981. 369
E. M. Clarke, O. Grumberg, and D. E. Long. Model Checking and Abstraction. In 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 343–354. ACM Press, 1992. 369
Dennis Dams, Rob Gerth, and Orna Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2), 1997. 376
R. de Nicola and F. Vaandrager. Three Logics for Branching Bisimulation. Journal of the Association of Computing Machinery, 42(2):458–487, March 1995. 372
P. R. Halmos. Measure Theory. D. van Norstrand Company, 1950. 370
J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press. Distinguished Dissertation Series, 1996. 370
M. Huth. The Interval Domain: A Matchmaker for aCTL and aPCTL. In M. Mislove, editor, 2nd US-Brazil joint workshop on the Formal Foundations of Software Systems held at Tulane University, New Orleans, Louisiana, November 13-16, 1997, volume 14 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999. 378
B. Jonsson and K. G. Larsen. Specification and Refinement of Probabilistic Processes. In Proceedings of the International Symposium on Logic in Computer Science, pages 266–277. IEEE Computer Society, IEEE Computer Society Press, July 1991. 370, 370, 371, 372, 378
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983. 373
K. G. Larsen. Modal Specifications. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 232–246. Springer Verlag, June 12-14, 1989 1989. International Workshop, Grenoble, France. 370, 373, 373, 373
K. G. Larsen and A. Skou. Bisimulation through Probabilistic Testing. Information and Computation, 94(1):1–28, September 1991. 370, 378
K. G. Larsen and B. Thomsen. A Modal Process Logic. In Third Annual Symposium on Logic in Computer Science, pages 203–210. IEEE Computer Society Press, 1988. 370, 370, 372, 372, 373, 377, 377
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. 369
R. Milner. Communication and Concurrency. Series in Computer Science. Prentice-Hall International, 1989. 369, 372, 377, 377, 377
R. E. Moore. Interval Analysis. Prentice-Hall, Englewood Cliffs, 1966. 372
C. Morgan, A. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325–353, May 1996. 378
M. Narashima, R. Cleaveland, and P. Iyer. Probabilistic Temporal Logics via the Modal Mu-Calculus. In W. Thomas, editor, Foundations of Software Science and Computation Structures, volume 1578 of Lecture Notes in Computer Science, pages 288–305. Springer Verlag, March 1999. 379
J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in cesar. In Proceedings of the fifth International Symposium on Programming, 1981. 369
D. S. Scott. Lattice Theory, Data Types and Semantics. In Formal Semantics of Programming Languages, pages 66–106. Prentice-Hall, 1972. 372
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huth, M. (1999). A Unifying Framework for Model Checking Labeled Kripke Structures, Modal Transition Systems, and Interval Transition Systems. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1999. Lecture Notes in Computer Science, vol 1738. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46691-6_30
Download citation
DOI: https://doi.org/10.1007/3-540-46691-6_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66836-7
Online ISBN: 978-3-540-46691-8
eBook Packages: Springer Book Archive