PhD dissertation

  Fragments of Fixpoint Logics: Automata and Expressiveness.
Facundo Carreiro. Institute for Logic, Language and Computation. University of Amsterdam, 2015. Supervisor: Yde Venema.

This dissertation studies the relative expressive power and properties of several fixpoint and second-order logics. We use the term fixpoint logic in a broad sense, referring to any logic which can encode some type of recursion, iteration or repetition. Our main objective is to systematically identify several important logics as precise fragments of other well-known logics. In order to accomplish this task, we develop automata-theoretic tools to analyze these fragments. The results of this dissertation provide new insight on the relationship of fixpoint and second-order logic and provides further evidence of the successful logic-automata connection.


   PDL Is the Bisimulation-Invariant Fragment of Weak Chain Logic.
Facundo Carreiro. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 341–352. (doi:10.1109/LICS.2015.40)

We introduce a new class of parity automata which, on trees, captures the expressive power of weak chain logic. This logic is a variant of monadic second-order logic which quantifies over finite chains. Using this new tool, we show that the bisimulation-invariant fragment of weak chain logic is equivalent to propositional dynamic logic.

   PDL inside the \(\mu\)-calculus: a syntactic and an automata-theoretic characterization.
Facundo Carreiro and Yde Venema. In Advances in Modal Logic 10, invited and contributed papers from the tenth conference on Advances in Modal Logic, held in Groningen, The Netherlands, August 5-8, 2014, pages 74–93. College Publications, 2014.

It is well known that Propositional Dynamic Logic (PDL) can be seen as a fragment of the modal \(\mu\)-calculus. In this paper we provide an exact syntactic characterization of the fragments of the \(\mu\)-calculus that correspond to PDL and to test-free PDL. In addition we give automata-theoretic characterizations for PDL, with and without tests, which shed light on the relation between these logics and the modal \(\mu\)-calculus and provide a new framework for the development of the theory of PDL.

   Weak MSO: Automata and expressiveness modulo bisimilarity.
Facundo Carreiro, Alessandro Facchini, Yde Venema, and Fabio Zanasi. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, Austria, July 14-18, 2014, pages 27. ACM, 2014. (doi:10.1145/2603088.2603101)

We prove that the bisimulation-invariant fragment of weak monadic second-order logic (WMSO) is equivalent to the fragment of the modal \(\mu\)-calculus where the application of the least fixpoint operator \(\mu p.\varphi\) is restricted to formulas \(\varphi\) that are continuous in p. Our proof is automata-theoretic in nature; in particular, we introduce a class of automata characterizing the expressive power of WMSO over tree models of arbitrary branching degree. The transition map of these automata is defined in terms of a logic \(FOE^\infty_1\) that is the extension of first-order logic with a generalized quantifier \(\exists^\infty\), where \(\exists^\infty x.\varphi\) means that there are infinitely many objects satisfying \(\varphi\). An important part of our work consists of a model-theoretic analysis of \(FOE^\infty_1\).

   Characterization, definability and separation via saturated models.
Carlos Areces, Facundo Carreiro, and Santiago Figueira. In Theoretical Computer Science, pages 537:72–86. June 2014. (doi:10.1016/j.tcs.2014.02.047)

Three important results about the expressivity of a modal logic L are the Characterization Theorem (that identifies a modal logic L as a fragment of a better known logic), the Definability Theorem (that provides conditions under which a class of L-models can be defined by a formula or a set of formulas of L), and the Separation Theorem (that provides conditions under which two disjoint classes of L-models can be separated by a class definable in L). We provide general conditions under which these results can be established for a given choice of model class and modal language whose expressivity is below first order logic. Besides some basic constraints that most modal logics easily satisfy, the fundamental condition that we require is that the class of \(\omega\)-saturated models in question has the Hennessy-Milner property with respect to the notion of observational equivalence under consideration. Given that the Characterization, finability and Separation theorems are among the cornerstones in the model theory of L, this property can be seen as a test that identifies the adequate notion of observational equivalence for a particular modal logic.

   Coalgebraic announcement logics.
Facundo Carreiro, Daniel Gorín, and Lutz Schröder. In 40th International Colloquium on Automata, Languages, and Programming (ICALP), volume 7966 of Lecture Notes in Computer Science, pages 101–112. 2013.

In epistemic logic, dynamic operators describe the evolution of the knowledge of participating agents through communication, one of the most basic forms of communication being public announcement. Semantically, dynamic operators correspond to transformations of the underlying model. While metatheoretic results on dynamic epistemic logic so far are largely limited to the setting of Kripke models, there is evident interest in extending its scope to non-relational modalities capturing, e.g., uncertainty or collaboration. We develop a generic framework for non-relational dynamic logic by adding dynamic operators to coalgebraic logic. We discuss a range of examples and establish basic results including bisimulation invariance, complexity, and a small model property.

   Beyond regularity for Presburger modal logics.
Facundo Carreiro and Stéphane Demri. In Selected Papers from the 9th Workshop on Advances in Modal Logics, pages 161–182. Copenhagen, Denmark, August 2012. College Publications.

Satisfiability problem for modal logic K augmented with quantifier-free Presburger and regularity constraints (EML) is known to be PSPACE-complete. In this paper, we consider its extension with nonregular constraints and more specifically those expressed by visibly pushdown languages (VPL). This class of languages is known to behave nicely, in particular when combined with Propositional Dynamic Logic (PDL). By extending EML, we show that decidability is preserved if we allow at most one positive VPL at each modal depth. By contrast, the presence of two VPL-contraints at the same modal depth or the presence of a negative occurrence of a single VPL-constraint leads to undecidability. This contrasts with decidability of PDL augmented with VPL-constraints.

   Basic model theory for memory logics.
Carlos Areces, Facundo Carreiro, Santiago Figueira, and Sergio Mera. In WoLLIC 2011, volume 6642 of Lecture Notes in Computer Science, pages 20–34. Springer Verlag, 2011.

Memory logics is a family of modal logics whose semantics is specified in terms of relational models enriched with additional data structure to represent a memory. The logical language includes a collection of operations to access and modify the data structure. In this paper we study basic model properties of memory logics, and prove results concerning characterization, definability and interpolation. While the first two properties hold for all memory logics introduced in this article, interpolation fails in most cases.

   On characterization, definability and \(\omega\)-saturated models.
Facundo Carreiro. In ICTAC 2011, volume 6916 of Lecture Notes in Computer Science, pages 62–76. Springer Verlag, 2011.

Two important classic results about modal expressivity are the Characterization and Definability theorems. We develop a general theory for modal logics below first order (in terms of expressivity) which exposes the following result: Characterization and Definability theorems hold for every (reasonable) modal logic whose omega-saturated models have the Hennessy-Milner property. The results are presented in a general version which is relativized to classes of models.