DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2017.29

Model-Checking Counting Temporal Logics on Flat Structures

Authors: Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract

We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.

Cite as

Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma. Model-Checking Counting Temporal Logics on Flat Structures. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{decker_et_al:LIPIcs.CONCUR.2017.29,
  author =	{Decker, Normann and Habermehl, Peter and Leucker, Martin and Sangnier, Arnaud and Thoma, Daniel},
  title =	{{Model-Checking Counting Temporal Logics on Flat Structures}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.29},
  URN =		{urn:nbn:de:0030-drops-77709},
  doi =		{10.4230/LIPIcs.CONCUR.2017.29},
  annote =	{Keywords: Counting Temporal Logic, Model checking, Flat Kripke Structure}
}

Document

DOI: 10.4230/LIPIcs.STACS.2012.242

Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree

Authors: Antoine Durand-Gasselin and Peter Habermehl

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Abstract

Many relational structures are automatically presentable, i.e. elements of the domain can be seen as words over a finite alphabet and equality and other atomic relations are represented with finite automata. The first-order theories over such structures are known to be primitive recursive, which is shown by the inductive construction of an automaton representing any relation definable in the first-order logic. We propose a general method based on Ehrenfeucht-Fraïssé games to give upper bounds on the size of these automata and on the time required to build them. We apply this method for two different automatic structures which have elementary decision procedures, Presburger Arithmetic and automatic structures of bounded degree. For the latter no upper bound on the size of the automata was known. We conclude that the very general and simple automata-based algorithm works well to decide the first-order theories over these structures.

Cite as

Antoine Durand-Gasselin and Peter Habermehl. Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 242-253, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{durandgasselin_et_al:LIPIcs.STACS.2012.242,
  author =	{Durand-Gasselin, Antoine and Habermehl, Peter},
  title =	{{Ehrenfeucht-Fra\"{i}ss\'{e} goes elementarily automatic for structures of bounded degree}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{242--253},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.242},
  URN =		{urn:nbn:de:0030-drops-34198},
  doi =		{10.4230/LIPIcs.STACS.2012.242},
  annote =	{Keywords: Automata-based decision procedures for logical theories, Automatic Structures, Ehrenfeucht-Fra\"{i}ss\'{e} Games, Logics, Complexity}
}

Search Results

Documents authored by Habermehl, Peter

Model-Checking Counting Temporal Logics on Flat Structures

Abstract

Cite as

Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree

Abstract

Cite as

Thanks for your feedback!

Could not send message