9 Search Results for "Rubin, Sasha"


Document
Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

Authors: Stefan Kiefer and Cas Widdershoven

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
We introduce a novel technique to analyse unambiguous Büchi automata quantitatively, and apply this to the model checking problem. It is based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant spectral radius. This method can replace a combinatorial procedure that dominates the computational complexity of the existing procedure by Baier et al. We analyse the complexity in detail, showing that, in terms of the set Q of states of the automaton, the new algorithm runs in time O(|Q|^4), improving on an efficient implementation of the combinatorial algorithm by a factor of |Q|.

Cite as

Stefan Kiefer and Cas Widdershoven. Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 82:1-82:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.MFCS.2019.82,
  author =	{Kiefer, Stefan and Widdershoven, Cas},
  title =	{{Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{82:1--82:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.82},
  URN =		{urn:nbn:de:0030-drops-110269},
  doi =		{10.4230/LIPIcs.MFCS.2019.82},
  annote =	{Keywords: Algorithms, Automata, Markov Chains, Matrix Semigroups}
}
Document
Long-Run Average Behavior of Vector Addition Systems with States

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NP-complete for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open.

Cite as

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Long-Run Average Behavior of Vector Addition Systems with States. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2019.27,
  author =	{Chatterjee, Krishnendu and Henzinger, Thomas A. and Otop, Jan},
  title =	{{Long-Run Average Behavior of Vector Addition Systems with States}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{27:1--27:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.27},
  URN =		{urn:nbn:de:0030-drops-109293},
  doi =		{10.4230/LIPIcs.CONCUR.2019.27},
  annote =	{Keywords: vector addition systems, mean-payoff, Diophantine inequalities}
}
Document
Reconfiguration and Message Losses in Parameterized Broadcast Networks

Authors: Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability problem which dually asks whether there exists an execution that visits a configuration exhibiting some given state of the broadcast protocol. Coverability is known to be undecidable for static networks, i.e. when the number of nodes and communication topology is fixed along executions. In contrast, it is decidable in PTIME when the communication topology may change arbitrarily along executions, that is for reconfigurable networks. Surprisingly, no lower nor upper bounds on the minimal number of nodes, or the minimal length of covering execution in reconfigurable networks, appear in the literature. In this paper we show tight bounds for cutoff and length, which happen to be linear and quadratic, respectively, in the number of states of the protocol. We also introduce an intermediary model with static communication topology and non-deterministic message losses upon sending. We show that the same tight bounds apply to lossy networks, although, reconfigurable executions may be linearly more succinct than lossy executions. Finally, we show NP-completeness for the natural optimisation problem associated with the cutoff.

Cite as

Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Reconfiguration and Message Losses in Parameterized Broadcast Networks. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2019.32,
  author =	{Bertrand, Nathalie and Bouyer, Patricia and Majumdar, Anirban},
  title =	{{Reconfiguration and Message Losses in Parameterized Broadcast Networks}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.32},
  URN =		{urn:nbn:de:0030-drops-109345},
  doi =		{10.4230/LIPIcs.CONCUR.2019.32},
  annote =	{Keywords: model checking, parameterized verification, broadcast networks}
}
Document
Quantifying Bounds in Strategy Logic

Authors: Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin

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


Abstract
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.

Cite as

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
Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable

Authors: Salvatore La Torre, Anca Muscholl, and Igor Walukiewicz

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


Abstract
Verification of concurrent systems is a difficult problem in general, and this is the case even more in a parametrized setting where unboundedly many concurrent components are considered. Recently, Hague proposed an architecture with a leader process and unboundedly many copies of a contributor process interacting over a shared memory for which safety properties can be effectively verified. All processes in Hague's setting are pushdown automata. Here, we extend it by considering other formal models and, as a main contribution, find very liberal conditions on the individual processes under which the safety problem is decidable: the only substantial condition we require is the effective computability of the downward closure for the class of the leader processes. Furthermore, our result allows for a hierarchical approach to constructing models of concurrent systems with decidable safety problem: networks with tree-like architecture, where each process shares a register with its children processes (and another register with its parent). Nodes in such networks can be for instance pushdown automata, Petri nets, or multi-pushdown systems with decidable reachability problem.

Cite as

Salvatore La Torre, Anca Muscholl, and Igor Walukiewicz. Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 72-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{latorre_et_al:LIPIcs.CONCUR.2015.72,
  author =	{La Torre, Salvatore and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{72--84},
  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.72},
  URN =		{urn:nbn:de:0030-drops-53813},
  doi =		{10.4230/LIPIcs.CONCUR.2015.72},
  annote =	{Keywords: Verification, parametrized systems, shared memory}
}
Document
Verification of Population Protocols

Authors: Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar

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


Abstract
Population protocols [Angluin et al., PODC, 2004] are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. While the predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? We prove that both problems are decidable. Our results also prove decidability of a natural question about home spaces of Petri nets.

Cite as

Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of Population Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 470-482, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2015.470,
  author =	{Esparza, Javier and Ganty, Pierre and Leroux, J\'{e}r\^{o}me and Majumdar, Rupak},
  title =	{{Verification of Population Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{470--482},
  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.470},
  URN =		{urn:nbn:de:0030-drops-53770},
  doi =		{10.4230/LIPIcs.CONCUR.2015.470},
  annote =	{Keywords: Population protocols, Petri nets, parametrized verification}
}
Document
Distributed Local Strategies in Broadcast Networks

Authors: Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier

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


Abstract
We study the problems of reaching a specific control state, or converging to a set of target states, in networks with a parameterized number of identical processes communicating via broadcast. To reflect the distributed aspect of such networks, we restrict our attention to executions in which all the processes must follow the same local strategy that, given their past performed actions and received messages, provides the next action to be performed. We show that the reachability and target problems under such local strategies are NP-complete, assuming that the set of receivers is chosen non-deterministically at each step. On the other hand, these problems become undecidable when the communication topology is a clique. However, decidability can be regained for reachability under the additional assumption that all processes are bound to receive the broadcast messages.

Cite as

Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Distributed Local Strategies in Broadcast Networks. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 44-57, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2015.44,
  author =	{Bertrand, Nathalie and Fournier, Paulin and Sangnier, Arnaud},
  title =	{{Distributed Local Strategies in Broadcast Networks}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{44--57},
  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.44},
  URN =		{urn:nbn:de:0030-drops-53796},
  doi =		{10.4230/LIPIcs.CONCUR.2015.44},
  annote =	{Keywords: Broadcast networks, parameterized verification, local strategies}
}
Document
Order-Invariant MSO is Stronger than Counting MSO in the Finite

Authors: Tobias Ganzow and Sasha Rubin

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


Abstract
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.

Cite as

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
Cardinality and counting quantifiers on omega-automatic structures

Authors: Lukasz Kaiser, Sasha Rubin, and Vince Bárány

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


Abstract
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.

Cite as

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}
}
  • Refine by Author
  • 3 Rubin, Sasha
  • 2 Bertrand, Nathalie
  • 1 Bouyer, Patricia
  • 1 Bárány, Vince
  • 1 Chatterjee, Krishnendu
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Design and analysis of algorithms
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Quantitative automata
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 2 parameterized verification
  • 1 $omega$-automata
  • 1 $omega$-automatic presentations
  • 1 $omega$-semigroups
  • 1 Algorithms
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 3 2015
  • 3 2019
  • 2 2008
  • 1 2018

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