Abstract
In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to the logics characterizing all the semantics in van Glabbeek’s branching-time spectrum.
Research supported by the project 001-ABEL-CM-2013 within the NILS Science and Sustainability Programme, the Spanish project STRONGSOFT TIN2012-39391-C04-04, and the projects Nominal SOS (project nr. 141558-051) and Decidability and Expressiveness for Interval Temporal Logics (project nr. 130802-051) of the Icelandic Research Fund.
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
References
Aceto, L., Della Monica, D., Fábregas, I., Ingólfsdóttir, A.: When are prime formulae characteristic? (extended version). http://www.icetcs.ru.is/dario/techrep/lc15.pdf
Aceto, L., Fábregas, I., de Frutos Escrig, D., Ingólfsdóttir, A., Palomino, M.: Graphical representation of covariant-contravariant modal formulas. In: Proceedings of the 18th EXPRESS. EPTCS, vol. 64, pp. 1–15 (2011)
Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York (2007)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42(1), 232–268 (1995)
Boudol, G., Larsen, K.G.: Graphical versus logical specifications. Theor. Comput. Sci. 106(1), 3–20 (1992)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Cleaveland, R., Steffen, B.: Computing behavioural relations, logically. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) Automata, Languages and Programming. LNCS, vol. 510, pp. 127–138. Springer, Heidelberg (1991)
de Frutos-Escrig, D., Gregorio-Rodríguez, C., Palomino, M., Romero-Hernández, D.: Unifying the linear time-branching time spectrum of process semantics. Logical Methods Comput. Sci. 9(2), 1–74 (2013)
van Glabbeek, R.J.: The linear time-branching time spectrum I: The semantics of concrete, sequential processes. In: Handbook of Process Algebra, pp. 3–99. Elsevier (2001)
Graf, S., Sifakis, J.: A modal characterization of observational congruence on finite terms of CCS. Inf. Control 68(1–3), 125–145 (1986)
Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371–384 (1976)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
Steffen, B., Ingólfsdóttir, A.: Characteristic formulae for processes with divergence. Inf. Comput. 110(1), 149–163 (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Della Monica, D., Fábregas, I., Ingólfsdóttir, A. (2015). When Are Prime Formulae Characteristic?. In: Italiano, G., Pighizzini, G., Sannella, D. (eds) Mathematical Foundations of Computer Science 2015. MFCS 2015. Lecture Notes in Computer Science(), vol 9234. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48057-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-662-48057-1_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48056-4
Online ISBN: 978-3-662-48057-1
eBook Packages: Computer ScienceComputer Science (R0)