4 Search Results for "Antonopoulos, Timos"

Document
DOI: 10.4230/LIPIcs.FSCD.2024.18
Representation of Peano Arithmetic in Separation Logic

Authors: Sohei Ito and Makoto Tatsuta

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.
Cite as

Sohei Ito and Makoto Tatsuta. Representation of Peano Arithmetic in Separation Logic. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ito_et_al:LIPIcs.FSCD.2024.18,
  author =	{Ito, Sohei and Tatsuta, Makoto},
  title =	{{Representation of Peano Arithmetic in Separation Logic}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.18},
  URN =		{urn:nbn:de:0030-drops-203476},
  doi =		{10.4230/LIPIcs.FSCD.2024.18},
  annote =	{Keywords: First order logic, Separation logic, Peano arithmetic, Presburger arithmetic}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.157
Domain Reasoning in TopKAT

Authors: Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.
Cite as

Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Domain Reasoning in TopKAT. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 157:1-157:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ICALP.2024.157,
  author =	{Zhang, Cheng and de Amorim, Arthur Azevedo and Gaboardi, Marco},
  title =	{{Domain Reasoning in TopKAT}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{157:1--157:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.157},
  URN =		{urn:nbn:de:0030-drops-203003},
  doi =		{10.4230/LIPIcs.ICALP.2024.157},
  annote =	{Keywords: Kleene algebra, Kleene Algebra With Tests, Kleene Algebra With Domain, Kleene Algebra With Top and Tests, Completeness, Decidability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.8
Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries

Authors: Dana Angluin, Timos Antonopoulos, and Dana Fisman

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
A Büchi automaton is strongly unambiguous if every word w ∈ Σ^ω has at most one final path. Many properties of strongly unambiguous Büchi automata (SUBAs) are known. They are fully expressive: every regular ω-language can be represented by a SUBA. Equivalence and containment of SUBAs can be decided in polynomial time. SUBAs may be exponentially smaller than deterministic Muller automata and may be exponentially bigger than deterministic Büchi automata. In this work we show that SUBAs can be learned in polynomial time using membership and certain non-proper equivalence queries, which implies that they are polynomially predictable with membership queries. In contrast, under plausible cryptographic assumptions, non-deterministic Büchi automata are not polynomially predictable with membership queries.
Cite as

Dana Angluin, Timos Antonopoulos, and Dana Fisman. Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{angluin_et_al:LIPIcs.CSL.2020.8,
  author =	{Angluin, Dana and Antonopoulos, Timos and Fisman, Dana},
  title =	{{Strongly Unambiguous B\"{u}chi Automata Are Polynomially Predictable With Membership Queries}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.8},
  URN =		{urn:nbn:de:0030-drops-116519},
  doi =		{10.4230/LIPIcs.CSL.2020.8},
  annote =	{Keywords: Polynomially predictable languages, Automata learning, Strongly unambiguous B\"{u}chi automata, Automata succinctness, Regular \omega-languages, Grammatical inference}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.10
Query Learning of Derived Omega-Tree Languages in Polynomial Time

Authors: Dana Angluin, Timos Antonopoulos, and Dana Fisman

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We present the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees. Specifically, our algorithm uses membership and equivalence queries to learn classes of omega-tree languages derived from weak regular omega-word languages in polynomial time. The method is a general polynomial time reduction of learning a class of derived omega-tree languages to learning the underlying class of omega-word languages, for any class of omega-word languages recognized by a deterministic Büchi acceptor. Our reduction, combined with the polynomial time learning algorithm of Maler and Pnueli [Maler and Pneuli, Inform. Comput., 1995] for the class of weak regular omega-word languages yields the main result. We also show that subset queries that return counterexamples can be implemented in polynomial time using subset queries that return no counterexamples for deterministic or non-deterministic finite word acceptors, and deterministic or non-deterministic Büchi omega-word acceptors. A previous claim of an algorithm to learn regular omega-trees due to Jayasrirani, Begam and Thomas [Jayasrirani et al., ICGI, 2008] is unfortunately incorrect, as shown in [Angluin, YALEU/DCS/TR-1528, 2016].
Cite as

Dana Angluin, Timos Antonopoulos, and Dana Fisman. Query Learning of Derived Omega-Tree Languages in Polynomial Time. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{angluin_et_al:LIPIcs.CSL.2017.10,
  author =	{Angluin, Dana and Antonopoulos, Timos and Fisman, Dana},
  title =	{{Query Learning of Derived Omega-Tree Languages in Polynomial Time}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{10:1--10:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.10},
  URN =		{urn:nbn:de:0030-drops-77022},
  doi =		{10.4230/LIPIcs.CSL.2017.10},
  annote =	{Keywords: Learning, queries, infinite trees, derived tree languages, reactive systems}
}
  • Refine by Author
  • 2 Angluin, Dana
  • 2 Antonopoulos, Timos
  • 2 Fisman, Dana
  • 1 Gaboardi, Marco
  • 1 Ito, Sohei
  • Show More...

  • Refine by Classification
  • 1 Theory of computation
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Programming logic
  • 1 Theory of computation → Separation logic

  • Refine by Keyword
  • 1 Automata learning
  • 1 Automata succinctness
  • 1 Completeness
  • 1 Decidability
  • 1 First order logic
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2024
  • 1 2017
  • 1 2020

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact