Abstract
The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment \(\square \)LTL of the logic LTL(EB), the integration of the UNTIL-fragment of Pnueli’s linear time temporal logic (LTL) and the logic of Event-B, in which the most commonly used liveness conditions can be expressed. For this fragment a sound set of derivation rules is developed, which is also complete under mild restrictions for Event-B machines.
F. Ferrarotti—The research of Flavio Ferrarotti has been funded by the Federal Ministry for Climate Action, Environment, Energy, Mobility, Innovation and Technology (BMK), the Federal Ministry for Digital and Economic Affairs (BMDW), and the State of Upper Austria in the frame of the COMET Module Dependable Production Environments with Software Security (DEPS) within the COMET - Competence Centers for Excellent Technologies Programme managed by Austrian Research Promotion Agency FFG.
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
Similar content being viewed by others
Notes
- 1.
It is commonly assumed that this choice is external, i.e. the values are provided by the environment and not by the machine itself.
- 2.
Note that this is a strong interpretation of until-formulae, as it includes that \(\chi \) eventually holds. If this requirement is dropped, i.e. we allow \(\psi \) to hold forever, we obtain a weak notion of until-formulae, usually denoted as \(\psi \, \mathcal{W} \, \chi \).
References
Abrial, J.R.: The B-book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Abrial, J.R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010). https://doi.org/10.1017/CBO9781139195881
Barwise, J.: Admissible Sets and Structures. Springer, Berlin, Heidelberg (1975). https://doi.org/10.1017/9781316717196
Blass, A., Gurevich, Y., Shelah, S.: Choiceless polynomial time. Ann. Pure Appl. Log. 100, 141–187 (1999)
Börger, E., Gervasi, V.: Structures of Computing - A Guide into a Practice-Oriented Theory. Springer, Berlin, Heidelberg, New York (2024). forthcoming. https://doi.org/10.1007/978-3-031-54358-6
Börger, E., Stärk, R.: Abstract State Machines. Springer, Berlin, Heidelberg, New York (2003). https://doi.org/10.1007/978-3-642-18216-7
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 196–215. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69850-0_12
Ferrarotti, F., Rivière, P., Schewe, K.D., Singh, N.K., Aït Ameur, Y.: A complete fragment of LTL(EB). CoRR abs/2401.16838 (2024). https://arxiv.org/abs/2401.16838
Ferrarotti, F., Schewe, K.D., Tec, L., Wang, Q.: A unifying logic for non-deterministic, parallel and concurrent Abstract State Machines. Ann. Math. Artif. Intell. 83(3–4), 321–349 (2018). https://doi.org/10.1007/s10472-017-9569-3
Hoang, T.S., Abrial, J.-R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 456–471. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_31
Kröger, F., Merz, S.: Temporal Logic and State Systems. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68635-4
Lamport, L.: Specifying Systems, The TLA\(^+\) Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)
Manna, Z., Pnueli, A.: Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comput. Program. 4(3), 257–289 (1984). https://doi.org/10.1016/0167-6423(84)90003--0
Merz, S.: On the logic of TLA\(^+\). Comput. Artif. Intell. 22(3–4), 351–379 (2003)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (FoCS 1977), pp. 46–57. IEEE Computer Society (1977). https://doi.org/10.1109/SFCS.1977.32
Rivière, P., Singh, N.K., Aït Ameur, Y., Dupont, G.: Formalising liveness properties in Event-B with the reflexive EB4EB framework. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods. NFM 2023. LNCS, vol. 13903, pp. 312–331. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33170-1_19
Schmalz, M.: Formalizing the Logic of Event-B. Ph.D. thesis, ETH Zürich (2012)
Stärk, R.F., Nanchen, S.: A logic for abstract state machines. J. Univ. Comput. Sci. 7(11), 980–1005 (2001)
Väänänen, J.: Second-order and higher-order logic. In: Stanford Encyclopedia of Philosophy (2019). https://plato.stanford.edu/entries/logic-higher-order/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Ferrarotti, F., Rivière, P., Schewe, KD., Singh, N.K., Ameur, Y.A. (2024). A Complete Fragment of LTL(EB). In: Meier, A., Ortiz, M. (eds) Foundations of Information and Knowledge Systems. FoIKS 2024. Lecture Notes in Computer Science, vol 14589. Springer, Cham. https://doi.org/10.1007/978-3-031-56940-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-031-56940-1_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-56939-5
Online ISBN: 978-3-031-56940-1
eBook Packages: Computer ScienceComputer Science (R0)