×

Modal logics for nominal transition systems. (English) Zbl 1509.68188

Summary: We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science
68V20 Formalization of mathematics in connection with theorem provers

Software:

CC-Pi
PDFBibTeX XMLCite
Full Text: arXiv Link

References:

[1] Samson Abramsky. A domain equation for bisimulation.Information and Computation, 92(2):161- 218, 1991. · Zbl 0718.68057
[2] Mart´ın Abadi and C´edric Fournet. Mobile values, new names, and secure communication. In Chris Hankin and Dave Schmidt, editors,Proceedings of POPL ’01, pages 104-115. ACM, · Zbl 1323.68398
[3] Mart´ın Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: the Spi calculus. Information and Computation, 148(1):1-70, 1999. · Zbl 0924.68073
[4] Ki Yung Ahn, Ross Horne, and Alwen Tiu. A characterisation of open bisimilarity using an intuitionistic modal logic. In Roland Meyer and Uwe Nestmann, editors,28th International · Zbl 1442.68121
[5] Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Proof techniques for cryptographic processes.SIAM Journal on Computing, 31(3):947-986, 2001. · Zbl 1017.68050
[6] Martin Berger, Kohei Honda, and Nobuko Yoshida. Completeness and logical full abstraction in modal logics for typed mobile processes. In Luca Aceto, Ivan Damg˚ard, Leslie Ann Goldberg, Magn´us M. Halld´orsson, Anna Ing´olfsd´ottir, and Igor Walukiewicz, editors,Automata, Languages · Zbl 1155.68472
[7] Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Bj¨orn Victor. Psi-calculi: a framework for mobile processes with nominal data and logic.Logical Methods in Computer Science, 7(1), · Zbl 1213.68399
[8] Maria Grazia Buscemi and Ugo Montanari. CC-Pi: A constraint-based language for specifying service level agreements. In Rocco De Nicola, editor,Proceedings of ESOP 2007, volume 4421 of · Zbl 1187.68063
[9] Maria Grazia Buscemi and Ugo Montanari. Open bisimulation for the concurrent constraint pi-calculus. In Sophia Drossopoulou, editor,Proceedings of ESOP 2008, volume 4960 ofLNCS, pages 254-268. Springer, 2008. · Zbl 1133.68384
[10] Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors,Interactive Theorem Proving - 5th International · Zbl 1416.68152
[11] Julian C. Bradfield and Perdita Stevens. Observational mu-calculus. Technical Report RS-99-5, BRICS, 1999. · Zbl 1059.68540
[12] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor,Logic of Programs, Workshop, · Zbl 0546.68014
[13] Sjoerd Cranen, Jan Friso Groote, and Michel Reniers. A linear translation from CTL* to the first-order modalµ-calculus.Theoretical Computer Science, 412(28):3129 - 3139, 2011. Festschrift in Honour of Jan Bergstra. · Zbl 1216.68188
[14] Matteo Cimini, Mohammad Reza Mousavi, Michel A. Reniers, and Murdoch J. Gabbay. Nominal SOS.Electronic Notes in Theoretical Computer Science, 286:103-116, September 2012. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics · Zbl 1342.68193
[15] Muffy Calder, Savi Maharaj, and Carron Shankland. A modal logic for full LOTOS based on symbolic transition systems.The Computer Journal, 45(1):55-61, 2002. · Zbl 1008.68081
[16] Mads Dam. Model checking mobile processes.Information and Computation, 129(1):35 - 51, 1996. · Zbl 0864.68036
[17] Rocco De Nicola and Michele Loreti. Multiple-labelled transition systems for nominal calculi and their logics.Mathematical Structures in Computer Science, 18(1):107-143, 2008. · Zbl 1141.68047
[18] E. Allen Emerson. Model checking and the Mu-calculus. In Neil Immerman and Phokion G. Kolaitis, editors,Descriptive Complexity and Finite Models, Proceedings of a DIMACS Workshop, · Zbl 0877.03020
[19] Ulrik Frendrup, Hans H¨uttel, and Jesper Nyholm Jensen. Modal logics for cryptographic processes.Electronic Notes in Theoretical Computer Science, 68(2):124-141, 2002. Proceedings of EXPRESS’02, 9th International Workshop on Expressiveness in Concurrency. · Zbl 1270.03038
[20] Ulrik Frendrup and Jesper Nyholm Jensen. Bisimilarity in the spi-calculus. Master’s thesis, Aalborg University, 2001. http://projekter.aau.dk/projekter/en/studentthesis/bisimilarity-in
[21] Murdoch J. Gabbay. Theπ-calculus in FM. In Fairouz D. Kamareddine, editor,Thirty Five Years of Automating Mathematics, pages 247-269. Springer Netherlands, Dordrecht, 2003. · Zbl 1063.68073
[22] Matthew Hennessy and Xinxin Liu. A modal logic for message passing processes.Acta Informatica, 32(4):375-393, 1995. · Zbl 0827.68102
[23] Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In J. W. de Bakker and Jan van Leeuwen, editors,Automata, Languages and Programming, 7th · Zbl 0441.68018
[24] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985. · Zbl 0629.68021
[25] Hans H¨uttel and Michael D. Pedersen. A logical characterisation of static equivalence.Electronic Notes in Theoretical Computer Science, 173:139-157, 2007. Proceedings of the 23rd Conference · Zbl 1316.68096
[26] ArildMartinMøllerHaugstad,AndersFranzTerkelsen,andThomasVindum.Amodallogicforthefusioncalculus.Unpublished,AalborgUniversity, http://vbn.aau.dk/ws/files/61067487/1149104946.pdf, 2006.
[27] Magnus Johansson, Jesper Bengtson, Joachim Parrow, and Bj¨orn Victor. Weak equivalences in psi-calculi. InProceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, · Zbl 1213.68399
[28] Bengt Jonsson, Ahmed Hussain Khan, and Joachim Parrow. Implementing a model checking algorithm by adapting existing automated tools. In Joseph Sifakis, editor,Automatic Verification
[29] Vasileios Koutavas, Maciej Gazda, and Matthew Hennessy. Distinguishing between communicating transactions.Information and Computation, 259:1 - 30, 2018. · Zbl 1388.68198
[30] Vasileios Koutavas and Matthew Hennessy. First-order reasoning for higher-order concurrency. Computer Languages, Systems & Structures, 38(3):242-277, 2012. · Zbl 1248.68355
[31] Bartek Klin and Mateusz Lelyk. Modal mu-calculus with atoms. In Valentin Goranko and Mads Dam, editors,26th EACSL Annual Conference on Computer Science Logic (CSL 2017), · Zbl 1434.03071
[32] Dexter Kozen. Results on the propositional mu-calculus.Theoretical Computer Science, 27(3):333 - 354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Pro · Zbl 0553.03007
[33] Casimir Kuratowski. Une m´ethode d’´elimination des nombres transfinis des raisonnements math´ematiques.Fundamenta Mathematicae, 3(1):76-108, 1922. · JFM 48.0205.04
[34] Leslie Lamport.Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, June 2002.
[35] Kim Guldstrand Larsen. Proof system for hennessy-milner logic with recursion. In Max Dauchet and Maurice Nivat, editors,CAAP ’88, 13th Colloquium on Trees in Algebra and Programming, · Zbl 0698.68014
[36] Robin Milner. A modal characterisation of observable machine-behaviour. In Egidio Astesiano and Corrado B¨ohm, editors,CAAP ’81, Trees in Algebra and Programming, 6th Colloquium, · Zbl 0474.68074
[37] Robin Milner.Communication and Concurrency. Prentice Hall, 1989. · Zbl 0683.68008
[38] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I.Information and Computation, 100(1):1-40, 1992. · Zbl 0752.68036
[39] Robin Milner, Joachim Parrow, and David Walker. Modal logics for mobile processes.Theoretical Computer Science, 114(1):149 - 171, 1993. · Zbl 0778.68033
[40] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 ofLNCS. Springer, 2002. · Zbl 0994.68131
[41] Michael Pedersen. Logics for the applied pi calculus. Master’s thesis, Aalborg University, 2006. BRICS RS-06-19.
[42] Andrew M. Pitts. Nominal logic, a first order theory of names and binding.Information and Computation, 186(2):165-193, 2003. · Zbl 1056.03014
[43] Andrew M. Pitts.Nominal Sets. Cambridge University Press, 2013. Cambridge Books Online. · Zbl 1297.68008
[44] Andrew M. Pitts, 2015. Personal communication.
[45] Joachim Parrow and Bj¨orn Victor. The fusion calculus: Expressiveness and symmetry in mobile processes. InProceedings of LICS 1998, pages 176-185. IEEE Computer Society Press, 1998.
[46] Joachim Parrow, Tjark Weber, Johannes Borgstr¨om, and Lars-Henrik Eriksson. Weak nominal modal logic. In Ahmed Bouajjani and Alexandra Silva, editors,Formal Techniques for Distributed · Zbl 1374.68339
[47] Davide Sangiorgi. A theory of bisimulation for theπ-calculus. In Eike Best, editor,Proceedings of CONCUR ’93, volume 715 ofLNCS, pages 127-142. Springer, 1993.
[48] Alex Simpson. Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS.The Journal of Logic and Algebraic Programming, 60-61:287-322, 2004. · Zbl 1072.68070
[49] Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications.Pacific Journal of Mathematics, 5(2):285-309, 1955. · Zbl 0064.26004
[50] Christian Urban and Cezary Kaliszyk. General bindings and alpha-equivalence in Nominal Isabelle.Logical Methods in Computer Science, 8(2), 2012. · Zbl 1242.68283
[51] Johan van Benthem.Modal Logic and Classical Logic. Bibliopolis, Naples, 1985. [WEP+16]Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgstr¨om, and Ram¯unas Gutkovas. Modal logics for nominal transition systems.Archive of Formal Proofs, October 2016. http://isa-afp.org/entries/Modal_Logics_for_NTS.shtml, Formal proof development.
[52] Lucian Wischik and Philippa Gardner. Explicit fusions.Theoretical Computer Science, 304(3):606- 630, 2005. · Zbl 1077.68066
[53] Xian Xu and Huan Long. A logical characterization for linear higher-order processes.Journal of Shanghai Jiaotong University (Science), 20(2):185-194, 2015.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.