Search Results

Documents authored by Kuusisto, Antti

Document
DOI: 10.4230/LIPIcs.CSL.2024.9
Descriptive Complexity for Neural Networks via Boolean Networks

Authors: Veeti Ahvonen, Damian Heiman, and Antti Kuusisto

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We investigate the descriptive complexity of a class of neural networks with unrestricted topologies and piecewise polynomial activation functions. We consider the general scenario where the running time is unlimited and floating-point numbers are used for simulating reals. We characterize these neural networks with a rule-based logic for Boolean networks. In particular, we show that the sizes of the neural networks and the corresponding Boolean rule formulae are polynomially related. In fact, in the direction from Boolean rules to neural networks, the blow-up is only linear. We also analyze the delays in running times due to the translations. In the translation from neural networks to Boolean rules, the time delay is polylogarithmic in the neural network size and linear in time. In the converse translation, the time delay is linear in both factors. We also obtain translations between the rule-based logic for Boolean networks, the diamond-free fragment of modal substitution calculus and a class of recursive Boolean circuits where the number of input and output gates match.
Cite as

Veeti Ahvonen, Damian Heiman, and Antti Kuusisto. Descriptive Complexity for Neural Networks via Boolean Networks. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ahvonen_et_al:LIPIcs.CSL.2024.9,
  author =	{Ahvonen, Veeti and Heiman, Damian and Kuusisto, Antti},
  title =	{{Descriptive Complexity for Neural Networks via Boolean Networks}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{9:1--9:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.9},
  URN =		{urn:nbn:de:0030-drops-196528},
  doi =		{10.4230/LIPIcs.CSL.2024.9},
  annote =	{Keywords: Descriptive complexity, neural networks, Boolean networks, floating-point arithmetic, logic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.9
Descriptive Complexity for Distributed Computing with Circuits

Authors: Veeti Ahvonen, Damian Heiman, Lauri Hella, and Antti Kuusisto

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We consider distributed algorithms in the realistic scenario where distributed message passing is operated by circuits. We show that within this setting, modal substitution calculus MSC precisely captures the expressive power of circuits. The result is established via constructing translations that are highly efficient in relation to size. We also observe that the coloring algorithm based on Cole-Vishkin can be specified by logarithmic size programs (and thus also logarithmic size circuits) in the bounded-degree scenario.
Cite as

Veeti Ahvonen, Damian Heiman, Lauri Hella, and Antti Kuusisto. Descriptive Complexity for Distributed Computing with Circuits. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ahvonen_et_al:LIPIcs.MFCS.2023.9,
  author =	{Ahvonen, Veeti and Heiman, Damian and Hella, Lauri and Kuusisto, Antti},
  title =	{{Descriptive Complexity for Distributed Computing with Circuits}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{9:1--9:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.9},
  URN =		{urn:nbn:de:0030-drops-185433},
  doi =		{10.4230/LIPIcs.MFCS.2023.9},
  annote =	{Keywords: Descriptive complexity, distributed computing, logic, graph coloring}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.38
Relating Description Complexity to Entropy

Authors: Reijo Jaakkola, Antti Kuusisto, and Miikka Vilander

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
We demonstrate some novel links between entropy and description complexity, a notion referring to the minimal formula length for specifying given properties. Let MLU be the logic obtained by extending propositional logic with the universal modality, and let GMLU be the corresponding extension with the ability to count. In the finite, MLU is expressively complete for specifying sets of variable assignments, while GMLU is expressively complete for multisets. We show that for MLU, the model classes with maximal Boltzmann entropy are the ones with maximal description complexity. Concerning GMLU, we show that expected Boltzmann entropy is asymptotically equivalent to expected description complexity multiplied by the number of proposition symbols considered. To contrast these results, we prove that this link breaks when we move to considering first-order logic FO over vocabularies with higher-arity relations. To establish the aforementioned result, we show that almost all finite models require relatively large FO-formulas to define them. Our results relate to links between Kolmogorov complexity and entropy, demonstrating a way to conceive such results in the logic-based scenario where relational structures are classified by formulas of different sizes.
Cite as

Reijo Jaakkola, Antti Kuusisto, and Miikka Vilander. Relating Description Complexity to Entropy. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jaakkola_et_al:LIPIcs.STACS.2023.38,
  author =	{Jaakkola, Reijo and Kuusisto, Antti and Vilander, Miikka},
  title =	{{Relating Description Complexity to Entropy}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{38:1--38:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.38},
  URN =		{urn:nbn:de:0030-drops-176903},
  doi =		{10.4230/LIPIcs.STACS.2023.38},
  annote =	{Keywords: finite model theory, entropy, formula size, randomness, formula size game}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.27
Complexity Classifications via Algebraic Logic

Authors: Reijo Jaakkola and Antti Kuusisto

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Complexity and decidability of logics is an active research area involving a wide range of different logical systems. We introduce an algebraic approach to complexity classifications of computational logics. Our base system GRA, or general relation algebra, is equiexpressive with first-order logic FO. It resembles cylindric algebra but employs a finite signature with only seven different operators, thus also giving a very succinct characterization of the expressive capacities of first-order logic. We provide a comprehensive classification of the decidability and complexity of the systems obtained by limiting the allowed sets of operators of GRA. We also discuss variants and extensions of GRA, and we provide algebraic characterizations of a range of well-known decidable logics.
Cite as

Reijo Jaakkola and Antti Kuusisto. Complexity Classifications via Algebraic Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jaakkola_et_al:LIPIcs.CSL.2023.27,
  author =	{Jaakkola, Reijo and Kuusisto, Antti},
  title =	{{Complexity Classifications via Algebraic Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.27},
  URN =		{urn:nbn:de:0030-drops-174880},
  doi =		{10.4230/LIPIcs.CSL.2023.27},
  annote =	{Keywords: Decidability, complexity, algebraic logic, fragments of first-order logic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.32
Model Checking and Validity in Propositional and Modal Inclusion Logics

Authors: Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the basic reasoning problems for modal and propositional dependence, independence, and inclusion logics.
Cite as

Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema. Model Checking and Validity in Propositional and Modal Inclusion Logics. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{hella_et_al:LIPIcs.MFCS.2017.32,
  author =	{Hella, Lauri and Kuusisto, Antti and Meier, Arne and Virtema, Jonni},
  title =	{{Model Checking and Validity in Propositional and Modal Inclusion Logics}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{32:1--32:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.32},
  URN =		{urn:nbn:de:0030-drops-81007},
  doi =		{10.4230/LIPIcs.MFCS.2017.32},
  annote =	{Keywords: Inclusion Logic, Model Checking, Complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.64
One-Dimensional Logic over Trees

Authors: Emanuel Kieronski and Antti Kuusisto

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
A one-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential quantifiers that leave at most one variable free. This fragment contains two-variable logic, and it is known that over words both formalisms have the same complexity and expressive power. Here we investigate the one-dimensional fragment over trees. We consider unranked unordered trees accessible by one or both of the descendant and child relations, as well as ordered trees equipped additionally with sibling relations. We show that over unordered trees the satisfiability problem is ExpSpace-complete when only the descendant relation is available and 2ExpTime-complete with both the descendant and child or with only the child relation. Over ordered trees the problem remains 2ExpTime-complete. Regarding expressivity, we show that over ordered trees and over unordered trees accessible by both the descendant and child the one-dimensional fragment is equivalent to the two-variable fragment with counting quantifiers.
Cite as

Emanuel Kieronski and Antti Kuusisto. One-Dimensional Logic over Trees. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 64:1-64:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kieronski_et_al:LIPIcs.MFCS.2017.64,
  author =	{Kieronski, Emanuel and Kuusisto, Antti},
  title =	{{One-Dimensional Logic over Trees}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{64:1--64:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.64},
  URN =		{urn:nbn:de:0030-drops-80658},
  doi =		{10.4230/LIPIcs.MFCS.2017.64},
  annote =	{Keywords: satisfiability, expressivity, trees, fragments of first-order logic}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.14
CTL with Finitely Bounded Semantics

Authors: Valentin Goranko, Antti Kuusisto, and Raine Rönnholm

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property. We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.
Cite as

Valentin Goranko, Antti Kuusisto, and Raine Rönnholm. CTL with Finitely Bounded Semantics. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{goranko_et_al:LIPIcs.TIME.2017.14,
  author =	{Goranko, Valentin and Kuusisto, Antti and R\"{o}nnholm, Raine},
  title =	{{CTL with Finitely Bounded Semantics}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.14},
  URN =		{urn:nbn:de:0030-drops-79325},
  doi =		{10.4230/LIPIcs.TIME.2017.14},
  annote =	{Keywords: CTL, finitely bounded semantics, tableaux, decidability}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICDT.2017.1
Rewritability in Monadic Disjunctive Datalog, MMSNP, and Expressive Description Logics (Invited Talk)

Authors: Cristina Feier, Antti Kuusisto, and Carsten Lutz

Published in: LIPIcs, Volume 68, 20th International Conference on Database Theory (ICDT 2017)

Abstract
We study rewritability of monadic disjunctive Datalog programs, (the complements of) MMSNP sentences, and ontology-mediated queries (OMQs) based on expressive description logics of the ALC family and on conjunctive queries. We show that rewritability into FO and into monadic Datalog (MDLog) are decidable, and that rewritability into Datalog is decidable when the original query satisfies a certain condition related to equality. We establish 2NExpTime-completeness for all studied problems except rewritability into MDLog for which there remains a gap between 2NExpTime and 3ExpTime. We also analyze the shape of rewritings, which in the MMSNP case correspond to obstructions, and give a new construction of canonical Datalog programs that is more elementary than existing ones and also applies to non-Boolean queries.
Cite as

Cristina Feier, Antti Kuusisto, and Carsten Lutz. Rewritability in Monadic Disjunctive Datalog, MMSNP, and Expressive Description Logics (Invited Talk). In 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{feier_et_al:LIPIcs.ICDT.2017.1,
  author =	{Feier, Cristina and Kuusisto, Antti and Lutz, Carsten},
  title =	{{Rewritability in Monadic Disjunctive Datalog, MMSNP, and Expressive Description Logics}},
  booktitle =	{20th International Conference on Database Theory (ICDT 2017)},
  pages =	{1:1--1:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-024-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{68},
  editor =	{Benedikt, Michael and Orsi, Giorgio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2017.1},
  URN =		{urn:nbn:de:0030-drops-70636},
  doi =		{10.4230/LIPIcs.ICDT.2017.1},
  annote =	{Keywords: FO-Rewritability, MDDLog, MMSNP, DL, ontology mediated queries}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.60
Decidability of Predicate Logics with Team Semantics

Authors: Juha Kontinen, Antti Kuusisto, and Jonni Virtema

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schoenfinkel-Ramsey prefix classes of dependence logic.
Cite as

Juha Kontinen, Antti Kuusisto, and Jonni Virtema. Decidability of Predicate Logics with Team Semantics. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 60:1-60:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kontinen_et_al:LIPIcs.MFCS.2016.60,
  author =	{Kontinen, Juha and Kuusisto, Antti and Virtema, Jonni},
  title =	{{Decidability of Predicate Logics with Team Semantics}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{60:1--60:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.60},
  URN =		{urn:nbn:de:0030-drops-64726},
  doi =		{10.4230/LIPIcs.MFCS.2016.60},
  annote =	{Keywords: team semantics, dependence logic, complexity, two-variable logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.597
Uniform One-Dimensional Fragments with One Equivalence Relation

Authors: Emanuel Kierónski and Antti Kuusisto

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
The uniform one-dimensional fragment U1 of first-order logic was introduced recently as a natural generalization of the two-variable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIME-complete satisfiability problem. In this paper we investigate two restrictions of U1 that still contain FO2. We call these logics RU1 and SU1, or the restricted and strongly restricted uniform one-dimensional fragments. We introduce Ehrenfeucht-Fraisse games for the logics and prove that while SU1 and RU1 are expressively equivalent, they are strictly contained in U1. Furthermore, we consider extensions of the logics SU1, RU1 and U1 with unrestricted use of a single built-in equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIME-complete for SU1(E) and 2NEXPTIME-complete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1.
Cite as

Emanuel Kierónski and Antti Kuusisto. Uniform One-Dimensional Fragments with One Equivalence Relation. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 597-615, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kieronski_et_al:LIPIcs.CSL.2015.597,
  author =	{Kier\'{o}nski, Emanuel and Kuusisto, Antti},
  title =	{{Uniform One-Dimensional Fragments with One Equivalence Relation}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{597--615},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.597},
  URN =		{urn:nbn:de:0030-drops-54418},
  doi =		{10.4230/LIPIcs.CSL.2015.597},
  annote =	{Keywords: two-variable logic, uniform one-dimensional fragments, complexity, expressivity, equivalence relations}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.452
Modal Logic and Distributed Message Passing Automata

Authors: Antti Kuusisto

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
In a recent article, Lauri Hella and co-authors identify a canonical connection between modal logic and deterministic distributed constant-time algorithms. The paper reports a variety of highly natural logical characterizations of classes of distributed message passing automata that run in constant time. The article leaves open the question of identifying related logical characterizations when the constant running time limitation is lifted. We obtain such a characterization for a class of finite message passing automata in terms of a recursive bisimulation invariant logic which we call modal substitution calculus (MSC). We also give a logical characterization of the related class A of infinite message passing automata by showing that classes of labelled directed graphs recognizable by automata in A are exactly the classes co-definable by a modal theory. A class C is co-definable by a modal theory if the complement of C is definable by a possibly infinite set of modal formulae. We also briefly discuss expressivity and decidability issues concerning MSC. We establish that MSC contains the Sigma^\mu_1 fragment of the modal \mu-calculus in the finite. We also observe that the single variable fragment MSC^1 of MSC is not contained in MSO, and that the SAT and FINSAT problems of MSC^1 are complete for PSPACE.
Cite as

Antti Kuusisto. Modal Logic and Distributed Message Passing Automata. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 452-468, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{kuusisto:LIPIcs.CSL.2013.452,
  author =	{Kuusisto, Antti},
  title =	{{Modal Logic and Distributed Message Passing Automata}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{452--468},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.452},
  URN =		{urn:nbn:de:0030-drops-42132},
  doi =		{10.4230/LIPIcs.CSL.2013.452},
  annote =	{Keywords: Modal logic, message passing automata, descriptive characterizations, distributed computing}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.470
Undecidable First-Order Theories of Affine Geometries

Authors: Antti Kuusisto, Jeremy Meyers, and Jonni Virtema

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (\beta) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,\beta) with unary predicates is decidable. We refute this conjecture by showing that for all n > 1, the FO-theory of monadic expansions of (R^n,\beta) is Pi^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,\beta), where T is a subset of R^n, and show that for each structure (T,\beta) in C, the FO-theory of the class of monadic expansions of (T,\beta) is undecidable. We then consider classes of expansions of structures (T,\beta) with restricted unary predicates, for example finite predicates, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivity of universal MSO and weak universal MSO over expansions of (R^n,\beta). While the logics are incomparable in general, over expansions of (R^n,\beta), formulae of weak universal MSO translate into equivalent formulae of universal MSO. An extended version of this article can be found on the ArXiv (arXiv:1208.4930v1).
Cite as

Antti Kuusisto, Jeremy Meyers, and Jonni Virtema. Undecidable First-Order Theories of Affine Geometries. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 470-484, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kuusisto_et_al:LIPIcs.CSL.2012.470,
  author =	{Kuusisto, Antti and Meyers, Jeremy and Virtema, Jonni},
  title =	{{Undecidable First-Order Theories of Affine Geometries}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{470--484},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.470},
  URN =		{urn:nbn:de:0030-drops-36910},
  doi =		{10.4230/LIPIcs.CSL.2012.470},
  annote =	{Keywords: Tarski’s geometry, undecidability, spatial logic, classical logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact