Abstract
The paper shows how to refine large-scale or even infinite transition systems so as to ensure certain desired properties. First, a given system is reduced into a smallish, finite bisimulation quotient. Second, the reduced system is refined in order to ensure a given property, using any known finite-state method. Third, the refined reduced system is expanded back into an adequate refinement of the system given initially. The proposed method is based on a Galois connection between systems and their quotients. It is applicable to various models and bisimulations and is illustrated with a few qualitative and quantitative properties.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press, Cambridge (2008)
Clarke, E., Grumberg, O., Peled, D.: Model checking, 3rd edn. MIT Press, Cambridge (2001)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Symp. Principles of Programming Languages, pp. 238–252. ACM, New York (1977)
Erné, M., Koslowski, J., Melton, A., Strecker, G.: A primer on Galois connections. In: Andima, S., et al. (eds.) Papers on general topology and its applications. 7th Summer Conf. Wisconsin. Annals New York Acad. Sci., New York, 704th edn., pp. 103–125 (1994)
Fernandez, J.-C.: An implementation of an efficient algorithm for bisimulation equivalence. Sci. Computer Programming 13(2-3), 219–236 (1989)
Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.J., Schmitt, A.: Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem. ACM Trans. Programming Languages and Systems 29(3), Article 17, 17–65 (2007)
Givan, R., Dean, T., Greig, M.: Equivalence notions and model minimization in Markov decision processes. Artificial Intell. J. 147(1-2), 163–223 (2003)
Glück, R., Möller, B., Sintzoff, M.: A semiring approach to equivalences, bisimulations and control. In: Berghammer, R., Jaoua, A.M., Möller, B. (eds.) RelMiCS 2009. LNCS, vol. 5827, pp. 134–149. Springer, Heidelberg (2009)
Gondran, M., Minoux, M.: Graphs, dioids and semirings: new models and algorithms. Springer, Heidelberg (2008)
Henzinger, T.A., Majumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Trans. Computational Logic 6, 1–32 (2005)
Kanellakis, P., Smolka, S.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86, 43–68 (1990)
Marchand, H., Pinchinat, S.: Supervisory control problem using symbolic bisimulation techniques. In: Proc. Amer. Control Conf., vol. 6, pp. 4067–4071 (2000)
Milner, R.: A calculus of communicating systems. Extended reprint of LNCS 92. University of Edinburgh, Laboratory for Foundations of Computer Science, Report ECS-LFCS-86-7 (1986)
Milner, R.: Operational and algebraic semantics of concurrent processes. In: van Leeuwen, J. (ed.) Formal models and semantics. Handbook of Theoretical Computer Sci., vol. B, pp. 1201–1242. Elsevier, Amsterdam (1990)
Sintzoff, M.: Synthesis of optimal control policies for some infinite-state transition systems. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 336–359. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Glück, R., Möller, B., Sintzoff, M. (2011). Model Refinement Using Bisimulation Quotients. In: Johnson, M., Pavlovic, D. (eds) Algebraic Methodology and Software Technology. AMAST 2010. Lecture Notes in Computer Science, vol 6486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17796-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-17796-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17795-8
Online ISBN: 978-3-642-17796-5
eBook Packages: Computer ScienceComputer Science (R0)