Document

**Published in:** LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics.

Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin. Quantifying Bounds in Strategy Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 23:1-23:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.CSL.2018.23, author = {Fijalkow, Nathana\"{e}l and Maubert, Bastien and Murano, Aniello and Rubin, Sasha}, title = {{Quantifying Bounds in Strategy Logic}}, booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}, pages = {23:1--23:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-088-0}, ISSN = {1868-8969}, year = {2018}, volume = {119}, editor = {Ghica, Dan R. and Jung, Achim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.23}, URN = {urn:nbn:de:0030-drops-96901}, doi = {10.4230/LIPIcs.CSL.2018.23}, annote = {Keywords: Prompt LTL, Strategy Logic, Model checking, Automata with counters} }

Document

**Published in:** LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

We compare the expressiveness of two extensions of monadic
second-order logic (MSO) over the class of finite structures. The
first, counting monadic second-order logic (CMSO), extends MSO with
first-order modulo-counting quantifiers, allowing the expression of
queries like ``the number of elements in the structure is even''.
The second extension allows the use of an additional binary
predicate, not contained in the signature of the queried structure,
that must be interpreted as an arbitrary linear order on its
universe, obtaining order-invariant MSO.
While it is straightforward that every CMSO formula can be
translated into an equivalent order-invariant MSO formula, the
converse had not yet been settled. Courcelle showed that for
restricted classes of structures both order-invariant MSO and CMSO
are equally expressive, but conjectured that, in general,
order-invariant MSO is stronger than CMSO.
We affirm this conjecture by presenting a class of structures that
is order-invariantly definable in MSO but not definable in CMSO.

Tobias Ganzow and Sasha Rubin. Order-Invariant MSO is Stronger than Counting MSO in the Finite. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 313-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{ganzow_et_al:LIPIcs.STACS.2008.1353, author = {Ganzow, Tobias and Rubin, Sasha}, title = {{Order-Invariant MSO is Stronger than Counting MSO in the Finite}}, booktitle = {25th International Symposium on Theoretical Aspects of Computer Science}, pages = {313--324}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-06-4}, ISSN = {1868-8969}, year = {2008}, volume = {1}, editor = {Albers, Susanne and Weil, Pascal}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1353}, URN = {urn:nbn:de:0030-drops-13535}, doi = {10.4230/LIPIcs.STACS.2008.1353}, annote = {Keywords: MSO, Counting MSO, order-invariance, expressiveness, Ehrenfeucht-Fraiss\'{e} game} }

Document

**Published in:** LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

We investigate structures that can be represented by
omega-automata, so called omega-automatic structures, and prove
that relations defined over such structures in first-order logic
expanded by the first-order quantifiers `there exist at most
$aleph_0$ many', 'there exist finitely many' and 'there exist $k$
modulo $m$ many' are omega-regular. The proof identifies certain
algebraic properties of omega-semigroups.
As a consequence an omega-regular equivalence relation of countable
index has an omega-regular set of representatives. This implies
Blumensath's conjecture that a countable structure with an
$omega$-automatic presentation can be represented using automata
on finite words. This also complements a very recent result of
Hj"orth, Khoussainov, Montalban and Nies showing that there is an
omega-automatic structure which has no injective presentation.

Lukasz Kaiser, Sasha Rubin, and Vince Bárány. Cardinality and counting quantifiers on omega-automatic structures. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 385-396, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.STACS.2008.1360, author = {Kaiser, Lukasz and Rubin, Sasha and B\'{a}r\'{a}ny, Vince}, title = {{Cardinality and counting quantifiers on omega-automatic structures}}, booktitle = {25th International Symposium on Theoretical Aspects of Computer Science}, pages = {385--396}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-06-4}, ISSN = {1868-8969}, year = {2008}, volume = {1}, editor = {Albers, Susanne and Weil, Pascal}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1360}, URN = {urn:nbn:de:0030-drops-13602}, doi = {10.4230/LIPIcs.STACS.2008.1360}, annote = {Keywords: \$omega\$-automatic presentations, \$omega\$-semigroups, \$omega\$-automata} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail