Search Results

Documents authored by Almagor, Shaull

Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.19
Synchronized CTL over One-Counter Automata

Authors: Shaull Almagor, Daniel Assa, and Udi Boker

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
We consider the model-checking problem of Synchronized Computation-Tree Logic (CTL+Sync) over One-Counter Automata (OCAs). CTL+Sync augments CTL with temporal operators that require several paths to satisfy properties in a synchronous manner, e.g., the property "all paths should eventually see p at the same time". The model-checking problem for CTL+Sync over finite-state Kripke structures was shown to be in 𝖯^{NP^NP}. OCAs are labelled transition systems equipped with a non-negative counter that can be zero-tested. Thus, they induce infinite-state systems whose computation trees are not regular. The model-checking problem for CTL over OCAs was shown to be PSPACE-complete. We show that the model-checking problem for CTL+Sync over OCAs is decidable. However, the upper bound we give is non-elementary. We therefore proceed to study the problem for a central fragment of CTL+Sync, extending CTL with operators that require all paths to satisfy properties in a synchronous manner, and show that it is in EXP^NEXP (and in particular in EXPSPACE), by exhibiting a certain "segmented periodicity" in the computation trees of OCAs.
Cite as

Shaull Almagor, Daniel Assa, and Udi Boker. Synchronized CTL over One-Counter Automata. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2023.19,
  author =	{Almagor, Shaull and Assa, Daniel and Boker, Udi},
  title =	{{Synchronized CTL over One-Counter Automata}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.19},
  URN =		{urn:nbn:de:0030-drops-193921},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.19},
  annote =	{Keywords: CTL, Synchronization, One Counter Automata, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.11
The Geometry of Reachability in Continuous Vector Addition Systems with States

Authors: Shaull Almagor, Arka Ghosh, Tim Leys, and Guillermo A. Pérez

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

Abstract
We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are "almost" Minkowski sums of convex cones and zonotopes generated by the vectors labelling the transitions of the VASS. We use the latter to prove that short so-called linear path schemes suffice as witnesses of reachability in continuous VASS. Then, we give new polynomial-time algorithms for the reachability problem for linear path schemes. Finally, we also establish that enriching the model with zero tests makes the reachability problem intractable already for linear path schemes of dimension two.
Cite as

Shaull Almagor, Arka Ghosh, Tim Leys, and Guillermo A. Pérez. The Geometry of Reachability in Continuous Vector Addition Systems with States. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.MFCS.2023.11,
  author =	{Almagor, Shaull and Ghosh, Arka and Leys, Tim and P\'{e}rez, Guillermo A.},
  title =	{{The Geometry of Reachability in Continuous Vector Addition Systems with States}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{11:1--11:13},
  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.11},
  URN =		{urn:nbn:de:0030-drops-185457},
  doi =		{10.4230/LIPIcs.MFCS.2023.11},
  annote =	{Keywords: Vector addition system with states, reachability, continuous approximation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.18
Determinization of One-Counter Nets

Authors: Shaull Almagor and Asaf Yeshurun

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
One-Counter Nets (OCNs) are finite-state automata equipped with a counter that is not allowed to become negative, but does not have zero tests. Their simplicity and close connection to various other models (e.g., VASS, Counter Machines and Pushdown Automata) make them an attractive model for studying the border of decidability for the classical decision problems. The deterministic fragment of OCNs (DOCNs) typically admits more tractable decision problems, and while these problems and the expressive power of DOCNs have been studied, the determinization problem, namely deciding whether an OCN admits an equivalent DOCN, has not received attention. We introduce four notions of OCN determinizability, which arise naturally due to intricacies in the model, and specifically, the interpretation of the initial counter value. We show that in general, determinizability is undecidable under most notions, but over a singleton alphabet (i.e., 1 dimensional VASS) one definition becomes decidable, and the rest become trivial, in that there is always an equivalent DOCN.
Cite as

Shaull Almagor and Asaf Yeshurun. Determinization of One-Counter Nets. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2022.18,
  author =	{Almagor, Shaull and Yeshurun, Asaf},
  title =	{{Determinization of One-Counter Nets}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{18:1--18:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir 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.CONCUR.2022.18},
  URN =		{urn:nbn:de:0030-drops-170812},
  doi =		{10.4230/LIPIcs.CONCUR.2022.18},
  annote =	{Keywords: Determinization, One-Counter Net, Vector Addition System, Automata, Semilinear}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.34
Concurrent Games with Multiple Topologies

Authors: Shaull Almagor and Shai Guendelman

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Concurrent multi-player games with ω-regular objectives are a standard model for systems that consist of several interacting components, each with its own objective. The standard solution concept for such games is Nash Equilibrium, which is a "stable" strategy profile for the players. In many settings, the system is not fully observable by the interacting components, e.g., due to internal variables. Then, the interaction is modelled by a partial information game. Unfortunately, the problem of whether a partial information game has an NE is not known to be decidable. A particular setting of partial information arises naturally when processes are assigned IDs by the system, but these IDs are not known to the processes. Then, the processes have full information about the state of the system, but are uncertain of the effect of their actions on the transitions. We generalize the setting above and introduce Multi-Topology Games (MTGs) - concurrent games with several possible topologies, where the players do not know which topology is actually used. We show that extending the concept of NE to these games can take several forms. To this end, we propose two notions of NE: Conservative NE, in which a player deviates if she can strictly add topologies to her winning set, and Greedy NE, where she deviates if she can win in a previously-losing topology. We study the properties of these NE, and show that the problem of whether a game admits them is decidable.
Cite as

Shaull Almagor and Shai Guendelman. Concurrent Games with Multiple Topologies. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2022.34,
  author =	{Almagor, Shaull and Guendelman, Shai},
  title =	{{Concurrent Games with Multiple Topologies}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{34:1--34:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir 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.CONCUR.2022.34},
  URN =		{urn:nbn:de:0030-drops-170973},
  doi =		{10.4230/LIPIcs.CONCUR.2022.34},
  annote =	{Keywords: Concurrent games, Nash Equilibrium, Symmetry, Partial information}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.3
Simulation by Rounds of Letter-To-Letter Transducers

Authors: Antonio Abu Nassar and Shaull Almagor

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
Letter-to-letter transducers are a standard formalism for modeling reactive systems. Often, two transducers that model similar systems differ locally from one another, by behaving similarly, up to permutations of the input and output letters within "rounds". In this work, we introduce and study notions of simulation by rounds and equivalence by rounds of transducers. In our setting, words are partitioned to consecutive subwords of a fixed length k, called rounds. Then, a transducer 𝒯₁ is k-round simulated by transducer 𝒯₂ if, intuitively, for every input word x, we can permute the letters within each round in x, such that the output of 𝒯₂ on the permuted word is itself a permutation of the output of 𝒯₁ on x. Finally, two transducers are k-round equivalent if they simulate each other. We solve two main decision problems, namely whether 𝒯₂ k-round simulates 𝒯₁ (1) when k is given as input, and (2) for an existentially quantified k. We demonstrate the usefulness of the definitions by applying them to process symmetry: a setting in which a permutation in the identities of processes in a multi-process system naturally gives rise to two transducers, whose k-round equivalence corresponds to stability against such permutations.
Cite as

Antonio Abu Nassar and Shaull Almagor. Simulation by Rounds of Letter-To-Letter Transducers. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{abunassar_et_al:LIPIcs.CSL.2022.3,
  author =	{Abu Nassar, Antonio and Almagor, Shaull},
  title =	{{Simulation by Rounds of Letter-To-Letter Transducers}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{3:1--3:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.3},
  URN =		{urn:nbn:de:0030-drops-157231},
  doi =		{10.4230/LIPIcs.CSL.2022.3},
  annote =	{Keywords: Transducers, Permutations, Parikh, Simulation, Equivalence}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.35
Process Symmetry in Probabilistic Transducers

Authors: Shaull Almagor

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
Model checking is the process of deciding whether a system satisfies a given specification. Often, when the setting comprises multiple processes, the specifications are over sets of input and output signals that correspond to individual processes. Then, many of the properties one wishes to specify are symmetric with respect to the processes identities. In this work, we consider the problem of deciding whether the given system exhibits symmetry with respect to the processes' identities. When the system is symmetric, this gives insight into the behaviour of the system, as well as allows the designer to use only representative specifications, instead of iterating over all possible process identities. Specifically, we consider probabilistic systems, and we propose several variants of symmetry. We start with precise symmetry, in which, given a permutation π, the system maintains the exact distribution of permuted outputs, given a permuted inputs. We proceed to study approximate versions of symmetry, including symmetry induced by small L_∞ norm, variants of Parikh-image based symmetry, and qualitative symmetry. For each type of symmetry, we consider the problem of deciding whether a given system exhibits this type of symmetry.
Cite as

Shaull Almagor. Process Symmetry in Probabilistic Transducers. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 35:1-35:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{almagor:LIPIcs.FSTTCS.2020.35,
  author =	{Almagor, Shaull},
  title =	{{Process Symmetry in Probabilistic Transducers}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{35:1--35:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.35},
  URN =		{urn:nbn:de:0030-drops-132764},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.35},
  annote =	{Keywords: Symmetry, Probabilistic Transducers, Model Checking, Permutations}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.38
Coverability in 1-VASS with Disequality Tests

Authors: Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional VASS. We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. In our main result we generalise the problem to allow disequality constraints on edges (i.e., we allow edges to be disabled if the accumulated weight is equal to a specific value). We show that in this case the vertex-to-vertex reachability problem is solvable in polynomial time even though a shortest path may have exponential length. In the language of VASS this means that control-state reachability is in polynomial time for 1-dimensional VASS with disequality tests.
Cite as

Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell. Coverability in 1-VASS with Disequality Tests. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2020.38,
  author =	{Almagor, Shaull and Cohen, Nathann and P\'{e}rez, Guillermo A. and Shirmohammadi, Mahsa and Worrell, James},
  title =	{{Coverability in 1-VASS with Disequality Tests}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{38:1--38:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.38},
  URN =		{urn:nbn:de:0030-drops-128501},
  doi =		{10.4230/LIPIcs.CONCUR.2020.38},
  annote =	{Keywords: Reachability, Vector addition systems with states, Weighted graphs}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.47
Parametrized Universality Problems for One-Counter Nets

Authors: Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural questions: 1) does there exist an initial counter value that makes the language universal? 2) does there exist a sufficiently high ceiling so that the bounded language is universal? Although the ordinary universality problem is decidable (and Ackermann-complete) and these parameterized variants seem to reduce to checking basic structural properties of the underlying automaton, we show that in fact both problems are undecidable. We also look into the complexities of the problems for several decidable subclasses, namely for unambiguous, and deterministic systems, and for those over a single-letter alphabet.
Cite as

Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke. Parametrized Universality Problems for One-Counter Nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 47:1-47:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2020.47,
  author =	{Almagor, Shaull and Boker, Udi and Hofman, Piotr and Totzke, Patrick},
  title =	{{Parametrized Universality Problems for One-Counter Nets}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{47:1--47:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.47},
  URN =		{urn:nbn:de:0030-drops-128592},
  doi =		{10.4230/LIPIcs.CONCUR.2020.47},
  annote =	{Keywords: Counter net, VASS, Unambiguous Automata, Universality}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.107
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.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
DOI: 10.4230/LIPIcs.STACS.2019.6
The Semialgebraic Orbit Problem

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

Published in: LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Abstract
The Semialgebraic Orbit Problem is a fundamental reachability question that arises in the analysis of discrete-time linear dynamical systems such as automata, Markov chains, recurrence sequences, and linear while loops. An instance of the problem comprises a dimension d in N, a square matrix A in Q^{d x d}, and semialgebraic source and target sets S,T subseteq R^d. The question is whether there exists x in S and n in N such that A^nx in T. The main result of this paper is that the Semialgebraic Orbit Problem is decidable for dimension d <= 3. Our decision procedure relies on separation bounds for algebraic numbers as well as a classical result of transcendental number theory - Baker’s theorem on linear forms in logarithms of algebraic numbers. We moreover argue that our main result represents a natural limit to what can be decided (with respect to reachability) about the orbit of a single matrix. On the one hand, semialgebraic sets are arguably the largest general class of subsets of R^d for which membership is decidable. On the other hand, previous work has shown that in dimension d=4, giving a decision procedure for the special case of the Orbit Problem with singleton source set S and polytope target set T would entail major breakthroughs in Diophantine approximation.
Cite as

Shaull Almagor, Joël Ouaknine, and James Worrell. The Semialgebraic Orbit Problem. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.STACS.2019.6,
  author =	{Almagor, Shaull and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{The Semialgebraic Orbit Problem}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Niedermeier, Rolf and Paul, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.6},
  URN =		{urn:nbn:de:0030-drops-102450},
  doi =		{10.4230/LIPIcs.STACS.2019.6},
  annote =	{Keywords: linear dynamical systems, Orbit Problem, first order theory of the reals}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.42
Effective Divergence Analysis for Linear Recurrence Sequences

Authors: Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We study the growth behaviour of rational linear recurrence sequences. We show that for low-order sequences, divergence is decidable in polynomial time. We also exhibit a polynomial-time algorithm which takes as input a divergent rational linear recurrence sequence and computes effective fine-grained lower bounds on the growth rate of the sequence.
Cite as

Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, and James Worrell. Effective Divergence Analysis for Linear Recurrence Sequences. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 42:1-42:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2018.42,
  author =	{Almagor, Shaull and Chapman, Brynmor and Hosseini, Mehran and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{Effective Divergence Analysis for Linear Recurrence Sequences}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{42:1--42:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.42},
  URN =		{urn:nbn:de:0030-drops-95802},
  doi =		{10.4230/LIPIcs.CONCUR.2018.42},
  annote =	{Keywords: Linear recurrence sequences, Divergence, Algebraic numbers, Positivity}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.114
O-Minimal Invariants for Linear Loops

Authors: Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
The termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Such deceptively simple questions also relate to a number of deep open problems, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this paper, we introduce the class of o-minimal invariants, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel's conjecture in transcendental number theory.
Cite as

Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell. O-Minimal Invariants for Linear Loops. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 114:1-114:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.ICALP.2018.114,
  author =	{Almagor, Shaull and Chistikov, Dmitry and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{O-Minimal Invariants for Linear Loops}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{114:1--114:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.114},
  URN =		{urn:nbn:de:0030-drops-91188},
  doi =		{10.4230/LIPIcs.ICALP.2018.114},
  annote =	{Keywords: Invariants, linear loops, linear dynamical systems, non-termination, o-minimality}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.24
The Polytope-Collision Problem

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

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

Abstract
The Orbit Problem consists of determining, given a matrix A in R^dxd and vectors x,y in R^d, whether there exists n in N such that A^n=y. This problem was shown to be decidable in a seminal work of Kannan and Lipton in the 1980s. Subsequently, Kannan and Lipton noted that the Orbit Problem becomes considerably harder when the target y is replaced with a subspace of R^d. Recently, it was shown that the problem is decidable for vector-space targets of dimension at most three, followed by another development showing that the problem is in PSPACE for polytope targets of dimension at most three. In this work, we take a dual look at the problem, and consider the case where the initial vector x is replaced with a polytope P_1, and the target is a polytope P_2. Then, the question is whether there exists n in N such that A^n P_1 intersection P_2 does not equal the empty set. We show that the problem can be decided in PSPACE for dimension at most three. As in previous works, decidability in the case of higher dimensions is left open, as the problem is known to be hard for long-standing number-theoretic open problems. Our proof begins by formulating the problem as the satisfiability of a parametrized family of sentences in the existential first-order theory of real-closed fields. Then, after removing quantifiers, we are left with instances of simultaneous positivity of sums of exponentials. Using techniques from transcendental number theory, and separation bounds on algebraic numbers, we are able to solve such instances in PSPACE.
Cite as

Shaull Almagor, Joël Ouaknine, and James Worrell. The Polytope-Collision Problem. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.ICALP.2017.24,
  author =	{Almagor, Shaull and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{The Polytope-Collision Problem}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{24:1--24:14},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.24},
  URN =		{urn:nbn:de:0030-drops-74521},
  doi =		{10.4230/LIPIcs.ICALP.2017.24},
  annote =	{Keywords: linear dynamical systems, orbit problem, algebraic algorithms}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.28
High-Quality Synthesis Against Stochastic Environments

Authors: Shaull Almagor and Orna Kupferman

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
In the classical synthesis problem, we are given a linear temporal logic (LTL) formula psi over sets of input and output signals, and we synthesize a transducer that realizes psi: with every sequence of input signals, the transducer associates a sequence of output signals so that the generated computation satisfies psi. One weakness of automated synthesis in practice is that it pays no attention to the quality of the synthesized system. Indeed, the classical setting is Boolean: a computation satisfies a specification or does not satisfy it. Accordingly, while the synthesized system is correct, there is no guarantee about its quality. In recent years, researchers have considered extensions of the classical Boolean setting to a quantitative one. The logic FLTL is a multi-valued logic that augments LTL with quality operators. The satisfaction value of an FLTL formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. Decision problems for LTL become search or optimization problems for FLTL. In particular, in the synthesis problem, the goal is to generate a transducer that satisfies the specification in the highest possible quality. Previous work considered the worst-case setting, where the goal is to maximize the quality of the computation with the minimal quality. We introduce and solve the stochastic setting, where the goal is to generate a transducer that maximizes the expected quality of a computation, subject to a given distribution of the input signals. Thus, rather than being hostile, the environment is assumed to be probabilistic, which corresponds to many realistic settings. We show that the problem is 2EXPTIME-complete, like classical LTL synthesis. The complexity stays 2EXPTIME also in two extensions we consider: one that maximizes the expected quality while guaranteeing that the minimal quality is, with probability 1, above a given threshold, and one that allows assumptions on the environment.
Cite as

Shaull Almagor and Orna Kupferman. High-Quality Synthesis Against Stochastic Environments. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CSL.2016.28,
  author =	{Almagor, Shaull and Kupferman, Orna},
  title =	{{High-Quality Synthesis Against Stochastic Environments}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.28},
  URN =		{urn:nbn:de:0030-drops-65688},
  doi =		{10.4230/LIPIcs.CSL.2016.28},
  annote =	{Keywords: Stochastic and Quantitative Synthesis, Markov Decision Process}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.9
Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis

Authors: Shaull Almagor, Orna Kupferman, and Yaron Velner

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
In Boolean synthesis, we are given an LTL specification, and the goal is to construct a transducer that realizes it against an adversarial environment. Often, a specification contains both Boolean requirements that should be satisfied against an adversarial environment, and multi-valued components that refer to the quality of the satisfaction and whose expected cost we would like to minimize with respect to a probabilistic environment. In this work we study, for the first time, mean-payoff games in which the system aims at minimizing the expected cost against a probabilistic environment, while surely satisfying an omega-regular condition against an adversarial environment. We consider the case the omega-regular condition is given as a parity objective or by an LTL formula. We show that in general, optimal strategies need not exist, and moreover, the limit value cannot be approximated by finite-memory strategies. We thus focus on computing the limit-value, and give tight complexity bounds for synthesizing epsilon-optimal strategies for both finite-memory and infinite-memory strategies. We show that our game naturally arises in various contexts of synthesis with Boolean and multi-valued objectives. Beyond direct applications, in synthesis with costs and rewards to certain behaviors, it allows us to compute the minimal sensing cost of omega-regular specifications -- a measure of quality in which we look for a transducer that minimizes the expected number of signals that are read from the input.
Cite as

Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2016.9,
  author =	{Almagor, Shaull and Kupferman, Orna and Velner, Yaron},
  title =	{{Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{9:1--9:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.9},
  URN =		{urn:nbn:de:0030-drops-61689},
  doi =		{10.4230/LIPIcs.CONCUR.2016.9},
  annote =	{Keywords: Stochastic and Quantitative Synthesis, Mean Payoff Games, Sensing.}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.380
The Sensing Cost of Monitoring and Synthesis

Authors: Shaull Almagor, Denis Kuperberg, and Orna Kupferman

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
In FSTTCS 2014, we introduced sensing as a new complexity measure for the complexity of regular languages. Intuitively, the sensing cost quantifies the detail in which a random input word has to be read by a deterministic automaton in order to decide its membership in the language. In this paper, we consider sensing in two principal applications of deterministic automata. The first is monitoring: we are given a computation in an on-line manner, and we have to decide whether it satisfies the specification. The second is synthesis: we are given a sequence of inputs in an on-line manner and we have to generate a sequence of outputs so that the resulting computation satisfies the specification. In the first, our goal is to design a monitor that handles all computations and minimizes the expected average number of sensors used in the monitoring process. In the second, our goal is to design a transducer that realizes the specification for all input sequences and minimizes the expected average number of sensors used for reading the inputs. We argue that the two applications require new and different frameworks for reasoning about sensing, and develop such frameworks. We focus on safety languages. We show that for monitoring, minimal sensing is attained by a monitor based on the minimal deterministic automaton for the language. For synthesis, however, the setting is more challenging: minimizing the sensing may require exponentially bigger transducers, and the problem of synthesizing a minimally-sensing transducer is EXPTIME-complete even for safety specifications given by deterministic automata.
Cite as

Shaull Almagor, Denis Kuperberg, and Orna Kupferman. The Sensing Cost of Monitoring and Synthesis. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 380-393, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2015.380,
  author =	{Almagor, Shaull and Kuperberg, Denis and Kupferman, Orna},
  title =	{{The Sensing Cost of Monitoring and Synthesis}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{380--393},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.380},
  URN =		{urn:nbn:de:0030-drops-56563},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.380},
  annote =	{Keywords: Automata, regular languages, omega-regular languages, complexity, sensing, minimization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.325
Repairing Multi-Player Games

Authors: Shaull Almagor, Guy Avni, and Orna Kupferman

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Synthesis is the automated construction of systems from their specifications. Modern systems often consist of interacting components, each having its own objective. The interaction among the components is modeled by a multi-player game. Strategies of the components induce a trace in the game, and the objective of each component is to force the game into a trace that satisfies its specification. This is modeled by augmenting the game with omega-regular winning conditions. Unlike traditional synthesis games, which are zero-sum, here the objectives of the components do not necessarily contradict each other. Accordingly, typical questions about these games concern their stability - whether the players reach an equilibrium, and their social welfare - maximizing the set of (possibly weighted) specifications that are satisfied. We introduce and study repair of multi-player games. Given a game, we study the possibility of modifying the objectives of the players in order to obtain stability or to improve the social welfare. Specifically, we solve the problem of modifying the winning conditions in a given concurrent multi-player game in a way that guarantees the existence of a Nash equilibrium. Each modification has a value, reflecting both the cost of strengthening or weakening the underlying specifications, as well as the benefit of satisfying specifications in the obtained equilibrium. We seek optimal modifications, and we study the problem for various omega-regular objectives and various cost and benefit functions. We analyze the complexity of the problem in the general setting as well as in one with a fixed number of players. We also study two additional types of repair, namely redirection of transitions and control of a subset of the players.
Cite as

Shaull Almagor, Guy Avni, and Orna Kupferman. Repairing Multi-Player Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 325-339, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2015.325,
  author =	{Almagor, Shaull and Avni, Guy and Kupferman, Orna},
  title =	{{Repairing Multi-Player Games}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{325--339},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.325},
  URN =		{urn:nbn:de:0030-drops-53741},
  doi =		{10.4230/LIPIcs.CONCUR.2015.325},
  annote =	{Keywords: Nash equilibrium, concurrent games, repair}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.161
Regular Sensing

Authors: Shaull Almagor, Denis Kuperberg, and Orna Kupferman

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
The size of deterministic automata required for recognizing regular and omega-regular languages is a well-studied measure for the complexity of languages. We introduce and study a new complexity measure, based on the sensing required for recognizing the language. Intuitively, the sensing cost quantifies the detail in which a random input word has to be read in order to decide its membership in the language. We show that for finite words, size and sensing are related, and minimal sensing is attained by minimal automata. Thus, a unique minimal-sensing deterministic automaton exists, and is based on the language's right-congruence relation. For infinite words, the minimal sensing may be attained only by an infinite sequence of automata. We show that the optimal limit cost of such sequences can be characterized by the language's right-congruence relation, which enables us to find the sensing cost of omega-regular languages in polynomial time.
Cite as

Shaull Almagor, Denis Kuperberg, and Orna Kupferman. Regular Sensing. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 161-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2014.161,
  author =	{Almagor, Shaull and Kuperberg, Denis and Kupferman, Orna},
  title =	{{Regular Sensing}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{161--173},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.161},
  URN =		{urn:nbn:de:0030-drops-48409},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.161},
  annote =	{Keywords: Automata, regular languages, omega-regular languages, complexity, sensing, minimization}
}
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