2 Search Results for "Kelmendi, Edon"


Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Invariants for Continuous Linear Dynamical Systems

Authors: Shaull Almagor, Edon Kelmendi, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)


Abstract
Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of error states. In this paper we study the problem of synthesising inductive invariants that are definable in o-minimal expansions of the ordered field of real numbers. In particular, assuming Schanuel’s conjecture in transcendental number theory, we establish effective synthesis of o-minimal invariants in the case of semi-algebraic error sets. Without using Schanuel’s conjecture, we give a procedure for synthesizing o-minimal invariants that contain all but a bounded initial segment of the orbit and are disjoint from a given semi-algebraic error set. We further prove that effective synthesis of semi-algebraic invariants that contain the whole orbit, is at least as hard as a certain open problem in transcendental number theory.

Cite as

Shaull Almagor, Edon Kelmendi, Joël Ouaknine, and James Worrell. Invariants for Continuous Linear Dynamical Systems. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 107:1-107:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.ICALP.2020.107,
  author =	{Almagor, Shaull and Kelmendi, Edon and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{Invariants for Continuous Linear Dynamical Systems}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{107:1--107:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.107},
  URN =		{urn:nbn:de:0030-drops-125141},
  doi =		{10.4230/LIPIcs.ICALP.2020.107},
  annote =	{Keywords: Invariants, continuous linear dynamical systems, continuous Skolem problem, safety, o-minimality}
}
Document
Emptiness of Zero Automata Is Decidable

Authors: Mikolaj Bojanczyk, Hugo Gimbert, and Edon Kelmendi

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)


Abstract
Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of MSO, called TMSO+zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero automata called nonzero automata. We prove that for every zero automaton there is an equivalent nonzero automaton of quadratic size and the emptiness problem of nonzero automata is decidable, with complexity co-NP. These results imply that TMSO+zero has decidable satisfiability.

Cite as

Mikolaj Bojanczyk, Hugo Gimbert, and Edon Kelmendi. Emptiness of Zero Automata Is Decidable. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 106:1-106:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.ICALP.2017.106,
  author =	{Bojanczyk, Mikolaj and Gimbert, Hugo and Kelmendi, Edon},
  title =	{{Emptiness of Zero Automata Is Decidable}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{106:1--106:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.106},
  URN =		{urn:nbn:de:0030-drops-74745},
  doi =		{10.4230/LIPIcs.ICALP.2017.106},
  annote =	{Keywords: tree automata, probabilistic automata, monadic second-order logic}
}
  • Refine by Author
  • 2 Kelmendi, Edon
  • 1 Almagor, Shaull
  • 1 Bojanczyk, Mikolaj
  • 1 Gimbert, Hugo
  • 1 Ouaknine, Joël
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Algebraic algorithms
  • 1 Mathematics of computing → Continuous functions
  • 1 Mathematics of computing → Continuous mathematics
  • 1 Software and its engineering → Formal software verification
  • 1 Theory of computation → Finite Model Theory
  • Show More...

  • Refine by Keyword
  • 1 Invariants
  • 1 continuous Skolem problem
  • 1 continuous linear dynamical systems
  • 1 monadic second-order logic
  • 1 o-minimality
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2017
  • 1 2020

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