Abstract
When we consider systems with process creation and exit, we have potentially infinite state systems where the number of processes alive at any state is unbounded. Properties of such systems are naturally specified using modal logics with quantification, but they are hard to verify even over finite state systems. In [11] we proposed \(\textsf {IQML}\), an implicitly quantified modal logic where we can have assertions of the form every live agent has an \(\alpha \)-successor, and presented a complete axiomatization of valid formulas. Here we show that model checking for \(\textsf {IQML}\) is efficient even when we consider systems with infinitely many processes, provided we can efficiently present such collections of processes, and check non-emptiness of intersection efficiently. As a case study, we present a model checking algorithm over systems in which at any state, the collection of live processes is regular.
Keywords
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 subscriptionsNotes
- 1.
The witnesses for the two conjuncts cannot be the same and hence at least two processes are required.
References
Abdulla, P.A., Aiswarya, C., Atig, M.F., Montali, M., Rezine, O.: Recency-bounded verification of dynamic database-driven systems. In: Proceedings of the 35th ACM Symposium on Principles of Database Systems (2016)
van Benthem, J., van Eijck, J., Stebletsova, V.: Modal logic, transition systems and processes. J. Log. Comput. 4(5), 811–855 (1994). https://doi.org/10.1093/logcom/4.5.811
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press, Cambridge (2001)
Fitting, M., Thalmann, L., Voronkov, A.: Term-modal logics. Studia Logica 69(1), 133–169 (2001)
Grove, A.J.: Naming and identity in epistemic logic Part II: a first-order logic for naming. Artif. Intell. 74(2), 311–350 (1995)
Grove, A.J., Halpern, J.Y.: Naming and identity in epistemic logics Part I: the propositional case. J. Log. Comput. 3(4), 345–378 (1993)
Hughes, M., Cresswell, G.: A New Introduction to Modal Logic. Routledge, Abingdon (1996)
Khan, M.A., Patel, V.S.: A formal study of a generalized rough set model based on relative approximations. In: Nguyen, H.S., Ha, Q.-T., Li, T., Przybyła-Kasperek, M. (eds.) IJCRS 2018. LNCS (LNAI), vol. 11103, pp. 502–510. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99368-3_39
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994). https://doi.org/10.1145/177492.177726
Padmanabha, A., Ramanujam, R.: Model checking a logic over systems with regular sets of processes. Developmental Aspects of Intelligent Adaptive Systems (Innovations in Software Engineering), CEUR Workshop Proceedings, vol. 1819 (2017)
Padmanabha, A., Ramanujam, R.: Propositional modal logic with implicit modal quantification. In: Khan, M.A., Manuel, A. (eds.) ICLA 2019. LNCS, vol. 11600, pp. 6–17. Springer, Heidelberg (2019). https://doi.org/10.1007/978-3-662-58771-3_2
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46–57. IEEE (1977)
Sipser, M.: Introduction to the Theory of Computation, vol. 2. Thomson Course Technology Boston (2006)
Wang, Y.: A new modal framework for epistemic logic. In: Proceedings Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2017, Liverpool, UK, 24–26 July 2017, pp. 515–534 (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Padmanabha, A., Ramanujam, R. (2020). Verifying Implicitly Quantified Modal Logic over Dynamic Networks of Processes. In: Hung, D., D´Souza, M. (eds) Distributed Computing and Internet Technology. ICDCIT 2020. Lecture Notes in Computer Science(), vol 11969. Springer, Cham. https://doi.org/10.1007/978-3-030-36987-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-36987-3_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-36986-6
Online ISBN: 978-3-030-36987-3
eBook Packages: Computer ScienceComputer Science (R0)