Scalar and vectorial \(\mu\)-calculus with atoms. (English) Zbl 1442.68108
Summary: We study an extension of modal \(\mu\)-calculus to sets with atoms and we study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show expressive limitations of atom-enriched \(\mu\)-calculi, and explain how their expressive power depends on the structure of atoms used, and on the choice between basic or vectorial syntax.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B45 | Modal logic (including the logic of norms) |
References:
| [1] | A. Arnold and D. Niwi´nski. Rudiments of µ-calculus. Studies in logic and the foundations of mathematics. |
| [2] | A. Bauer and P. L. Lumsdaine. On the bourbaki-witt principle in toposes. In Mathematical Proceedings of the Cambridge Philosophical Society, volume 155, pages 87-99. Cambridge University Press, 2013. · Zbl 1286.03164 |
| [3] | M. Boja´nczyk, B. Klin, and S. Lasota. Automata theory in nominal sets. Log. Meth. Comp. Sci., 10, 2014. · Zbl 1338.68140 |
| [4] | M. Boja´nczyk and T. Place. Toward model theory with data values. In Procs. ICALP 2012 Part II, volume 7392 of Lecture Notes in Computer Science, pages 116-127, 2012. · Zbl 1367.03051 |
| [5] | J. Bradfield and C.Stirling. Modal mu-calculi. In Handbook of Modal Logic, volume 3, pages 721 - 756. Elsevier, 2007. · Zbl 1002.03021 |
| [6] | J. Bradfield and C. Stirling. Modal logics and mu-calculi: an introduction. In Handbook of Process Algebra, pages 293-330. North-Holland, 2001. · Zbl 1002.03021 |
| [7] | J. Bradfield and I. Walukiewicz. The mu-calculus and model-checking. In H. Veith E. Clarke, T. Henzinger, editor, Handbook of Model Checking. Springer-Verlag, 2015. · Zbl 1392.68236 |
| [8] | C. Carapelle and M. Lohrey. Temporal logics with local constraints (invited talk). In Procs. CSL 2015, volume 41 of LIPIcs, pages 2-13, 2015. · Zbl 1373.03020 |
| [9] | V. Ciancia and U. Montanari. Symmetries, local names and dynamic (de)-allocation of names. Inf. Comput., 208(12):1349-1367, 2010. · Zbl 1207.68223 |
| [10] | S. Cranen, J. F. Groote, and M. Reniers. A linear translation from CTL∗to the first-order modal µ-calculus. Theoretical Computer Science, 412(28):3129 - 3139, 2011. · Zbl 1216.68188 |
| [11] | M. Dam. Model checking mobile processes. Information and Computation, 129(1):35-51, 1996. · Zbl 0864.68036 |
| [12] | R. De Nicola and M. Loreti. Multiple-labelled transition systems for nominal calculi and their logics. Mathematical Structures in Computer Science, 18(01):107-143, 2008. · Zbl 1141.68047 |
| [13] | S. Demri and D. D’Souza. An automata-theoretic approach to constraint LTL. Inf. Comput., 205(3):380- 415, 2007. · Zbl 1113.03015 |
| [14] | S. Demri, D. D’Souza, and R. Gascon. Temporal logics of repeating values. J. Log. Comput., 22(5):1059- 1096, 2012. · Zbl 1279.68203 |
| [15] | S. Demri, D. Figueira, and M. Praveen. Reasoning about data repetitions with counter systems. Logical Methods in Computer Science, 12(3), 2016. · Zbl 1366.68202 |
| [16] | S. Demri and R. Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. · Zbl 1351.68158 |
| [17] | S. Demri, R. Lazic, and D. Nowak. On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput., 205(1):2-24, 2007. · Zbl 1116.03014 |
| [18] | E. A. Emerson and J. Y. Halpern. “sometimes” and “not never” revisited: On branching versus linear time temporal logic. J. ACM, 33(1):151-178, 1986. · Zbl 0629.68020 |
| [19] | G.-L. Ferrari, S. Gnesi, U. Montanari, and M. Pistore. A model-checking verification environment for mobile processes. ACM Transactions on Software Engineering and Methodology, 12(4):440-473, 2003. |
| [20] | D. Figueira. Alternating register automata on finite words and trees. Logical Methods in Computer Science, 8(1), 2012. · Zbl 1238.68074 |
| [21] | D. Figueira and L. Segoufin. Future-looking logics on data words and trees. In Procs. MFCS 2009, volume 5734 of Lecture Notes in Computer Science, pages 331-343, 2009. · Zbl 1250.03050 |
| [22] | N. Francez and M. Kaminski. Finite-memory automata. TCS, 134(2):329-363, 1994. · Zbl 0938.68711 |
| [23] | M. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Asp. Comput., 13(3-5):341-363, 2002. · Zbl 1001.68083 |
| [24] | J. F. Groote and R. Mateescu. Verification of temporal properties of processes in a setting with data. In Procs. AMAST’99, pages 74-90, 1999. · Zbl 0926.03036 |
| [25] | J. F. Groote and T. AC Willemse. Model-checking processes with data. Science of Computer Programming, 56(3):251-273, 2005. · Zbl 1082.68067 |
| [26] | M. Jurdzinski and R. Lazic. Alternating automata on data trees and xpath satisfiability. ACM Trans. Comput. Log., 12(3):19:1-19:21, 2011. · Zbl 1351.68141 |
| [27] | B. Klin, E. Kopczy´nski, J. Ochremiak, and S. Toru´nczyk. Locally finite constraint satisfaction problems. In Procs. LICS 2015, pages 475-486, 2015. · Zbl 1394.68186 |
| [28] | B. Klin and M. Le lyk. Modal µ-Calculus with Atoms. In Procs. CSL 2017, volume 82 of LIPIcs, pages 30:1-30:21, 2017. |
| [29] | B. Klin and M. Szynwelski. SMT solving for functional programming over infinite structures. In MFSP, · Zbl 1477.68072 |
| [30] | E. Kopczy´nski and S. Toru´nczyk. Lois: Syntax and semantics. In Procs. of POPL 2017, pages 586-598, 2017. · Zbl 1380.68125 |
| [31] | D. Kozen. Results on the propositional µ-calculus. Theor. Comp. Sci., 27(3):333 - 354, 1983. · Zbl 0553.03007 |
| [32] | Hui-Min Lin. Predicate µ-calculus for mobile ambients. Journal of Computer Science and Technology, 20(1):95-104, 2005. |
| [33] | S. L¨osch and A. M. Pitts. Denotational semantics with nominal scott domains. J. ACM, 61(4):27:1-27:46, 2014. · Zbl 1321.68202 |
| [34] | F. Neven, T. Schwentick, and V. Vianu. Towards regular languages over infinite alphabets. In MFCS, pages 560-572, 2001. · Zbl 0999.68110 |
| [35] | J. Ochremiak. Extended constraint satisfaction problems. PhD thesis, University of Warsaw, 2016. |
| [36] | J. Parrow, J. Borgstr¨om, L.-H. Eriksson, R. Gutkovas, and T. Weber. Modal logics for nominal transition systems. In Procs. CONCUR 2015, volume 42 of LIPIcs, pages 198-211, 2015. · Zbl 1374.68339 |
| [37] | A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. · Zbl 1297.68008 |
| [38] | L. Segoufin. Automata and logics for words and trees over an infinite alphabet. In Procs. CSL 2006, volume 4207 of Lecture Notes in Computer Science, pages 41-57, 2006. · Zbl 1225.68103 |
| [39] | W. Thomas and T. Wilke. Automata, logics, and infinite games: A guide to current research. Bulletin of Symbolic Logic, 10(1):114-115, 2004. |
| [40] | N. Tzevelekos. Fresh-register automata. SIGPLAN Not., 46(1):295-306, 2011. · Zbl 1284.68368 |
| [41] | Y. Venema. Lectures on the modal µ-calculus. ILLC, Univ. of Amsterdam, 2007. |
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.
