Search Results

Documents authored by Gastin, Paul

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.5
MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm

Authors: S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since timed automata tools do not handle alternation, existing methods perform an additional step of converting the alternating timed automata into timed automata. This "de-alternation" step proceeds by an intricate finite abstraction of the space of configurations of the alternating automaton. Recently, a model of generalized timed automata (GTA) has been proposed. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. An attractive feature of GTAs is the presence of future clocks which act like timers that guess a time to an event and stay alive until a timeout. Future clocks seem to provide another natural way to implement the guess-and-check: start the future clock with a guessed time to an event and check its occurrence using a timeout. Indeed, using this feature, we provide a new concise translation from MITL to GTA. In particular, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art. Thanks to this conversion, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. Due to the presence of future clocks, there is no finite time-abstract bisimulation (region equivalence) for GTAs, whereas liveness algorithms for timed automata crucially rely on the presence of the finite region equivalence. As our second contribution, we provide a new zone-based algorithm for checking Büchi non-emptiness in GTAs, which circumvents this fundamental challenge.
Cite as

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2024.5,
  author =	{Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
  title =	{{MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.5},
  URN =		{urn:nbn:de:0030-drops-207774},
  doi =		{10.4230/LIPIcs.CONCUR.2024.5},
  annote =	{Keywords: MITL model checking, timed automata, zones, liveness}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.21
Reversible Transducers over Infinite Words

Authors: Luc Dartois, Paul Gastin, Loïc Germerie Guizouarn, R. Govind, and Shankaranarayanan Krishna

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification. An important result by Dartois et al. [Luc Dartois et al., 2017] shows that composition of two-way transducers enjoy a polynomial composition when the underlying transducer is reversible, that is, if they are both deterministic and co-deterministic. This is a major improvement over general deterministic two-way transducers, for which composition causes a doubly exponential blow-up in the size of the inputs in general. Moreover, they show that reversible two-way transducers have the same expressiveness as deterministic two-way transducers. However, the notion of reversible two-way transducers over infinite words as well as the question of their expressiveness were not studied yet. In this article, we introduce the class of reversible two-way transducers over infinite words and show that they enjoy the same expressive power as deterministic two-way transducers over infinite words. This is done through a non-trivial, effective construction inducing a single exponential blow-up in the set of states. Further, we also prove that composing two reversible two-way transducers over infinite words incurs only a polynomial complexity, thereby providing an efficient procedure for composition of transducers over infinite words.
Cite as

Luc Dartois, Paul Gastin, Loïc Germerie Guizouarn, R. Govind, and Shankaranarayanan Krishna. Reversible Transducers over Infinite Words. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dartois_et_al:LIPIcs.CONCUR.2024.21,
  author =	{Dartois, Luc and Gastin, Paul and Germerie Guizouarn, Lo\"{i}c and Govind, R. and Krishna, Shankaranarayanan},
  title =	{{Reversible Transducers over Infinite Words}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{21:1--21:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.21},
  URN =		{urn:nbn:de:0030-drops-207932},
  doi =		{10.4230/LIPIcs.CONCUR.2024.21},
  annote =	{Keywords: Transducers, Regular functions, Reversibility, Composition, SSTs}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2022.1
CONCUR Test-Of-Time Award 2022 (Invited Paper)

Authors: Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi

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

Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the four papers that received the Award in 2022.
Cite as

Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi. CONCUR Test-Of-Time Award 2022 (Invited Paper). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 1:1-1:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{castellani_et_al:LIPIcs.CONCUR.2022.1,
  author =	{Castellani, Ilaria and Gastin, Paul and Kupferman, Orna and Randour, Mickael and Sangiorgi, Davide},
  title =	{{CONCUR Test-Of-Time Award 2022}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{1:1--1:3},
  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.1},
  URN =		{urn:nbn:de:0030-drops-170644},
  doi =		{10.4230/LIPIcs.CONCUR.2022.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.13
Simulations for Event-Clock Automata

Authors: S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan

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

Abstract
Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied in [Gilles Geeraerts et al., 2011; Gilles Geeraerts et al., 2014], where the authors also proposed a solution using zone extrapolations. In this paper, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the 𝒢-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.
Cite as

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. Simulations for Event-Clock Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2022.13,
  author =	{Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
  title =	{{Simulations for Event-Clock Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{13:1--13: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.13},
  URN =		{urn:nbn:de:0030-drops-170766},
  doi =		{10.4230/LIPIcs.CONCUR.2022.13},
  annote =	{Keywords: Event-clock automata, verification, zones, simulations, reachability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.28
Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages

Authors: Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil

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

Abstract
One of the main motivations for this work is to obtain a distributed Krohn-Rhodes theorem for Mazurkiewicz traces. Concretely, we focus on the recently introduced operation of local cascade product of asynchronous automata and ask if every regular trace language can be accepted by a local cascade product of "simple" asynchronous automata. Our approach crucially relies on the development of a local and past-oriented propositional dynamic logic (LocPastPDL) over traces which is shown to be expressively complete with respect to all regular trace languages. An event-formula of LocPastPDL allows to reason about the causal past of an event and a path-formula of LocPastPDL, localized at a process, allows to march along the sequence of past-events in which that process participates, checking for local regular patterns interspersed with local tests of other event-formulas. We also use additional constant formulas to compare the leading process events from the causal past. The new logic LocPastPDL is of independent interest, and the proof of its expressive completeness is rather subtle. Finally, we provide a translation of LocPastPDL formulas into local cascade products. More precisely, we show that every LocPastPDL formula can be computed by a restricted local cascade product of the gossip automaton and localized 2-state asynchronous reset automata and localized asynchronous permutation automata.
Cite as

Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.CONCUR.2022.28,
  author =	{Adsul, Bharat and Gastin, Paul and Sarkar, Saptarshi and Weil, Pascal},
  title =	{{Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{28:1--28:19},
  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.28},
  URN =		{urn:nbn:de:0030-drops-170915},
  doi =		{10.4230/LIPIcs.CONCUR.2022.28},
  annote =	{Keywords: Mazurkiewicz traces, propositional dynamic logic, regular trace languages, asynchronous automata, cascade product, Krohn Rhodes theorem}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.34
Weighted Tiling Systems for Graphs: Evaluation Complexity

Authors: C. Aiswarya and Paul Gastin

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

Abstract
We consider weighted tiling systems to represent functions from graphs to a commutative semiring such as the Natural semiring or the Tropical semiring. The system labels the nodes of a graph by its states, and checks if the neighbourhood of every node belongs to a set of permissible tiles, and assigns a weight accordingly. The weight of a labeling is the semiring-product of the weights assigned to the nodes, and the weight of the graph is the semiring-sum of the weights of labelings. We show that we can model interesting algorithmic questions using this formalism - like computing the clique number of a graph or computing the permanent of a matrix. The evaluation problem is, given a weighted tiling system and a graph, to compute the weight of the graph. We study the complexity of the evaluation problem and give tight upper and lower bounds for several commutative semirings. Further we provide an efficient evaluation algorithm if the input graph is of bounded tree-width.
Cite as

C. Aiswarya and Paul Gastin. Weighted Tiling Systems for Graphs: Evaluation Complexity. 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. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aiswarya_et_al:LIPIcs.FSTTCS.2020.34,
  author =	{Aiswarya, C. and Gastin, Paul},
  title =	{{Weighted Tiling Systems for Graphs: Evaluation Complexity}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{34:1--34:17},
  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.34},
  URN =		{urn:nbn:de:0030-drops-132753},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.34},
  annote =	{Keywords: Weighted graph tiling, tiling automata, Evaluation, Complexity, Tree-width}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.47
Reachability for Updatable Timed Automata Made Faster and More Effective

Authors: Paul Gastin, Sayan Mukherjee, and B Srivathsan

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

Abstract
Updatable timed automata (UTA) are extensions of classical timed automata that allow special updates to clock variables, like x: = x - 1, x : = y + 2, etc., on transitions. Reachability for UTA is undecidable in general. Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed to compute a set of clock constraints at each state; in the second phase, reachable sets of configurations, called zones, are enumerated. In this work, we improve the algorithm for the static analysis. Compared to the existing algorithm, our method computes smaller sets of constraints and guarantees termination for more UTA, making reachability faster and more effective. As the main application, we get an alternate proof of decidability and a more efficient algorithm for timed automata with bounded subtraction, a class of UTA widely used for modelling scheduling problems. We have implemented our procedure in the tool TChecker and conducted experiments that validate the benefits of our approach.
Cite as

Paul Gastin, Sayan Mukherjee, and B Srivathsan. Reachability for Updatable Timed Automata Made Faster and More Effective. 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. 47:1-47:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gastin_et_al:LIPIcs.FSTTCS.2020.47,
  author =	{Gastin, Paul and Mukherjee, Sayan and Srivathsan, B},
  title =	{{Reachability for Updatable Timed Automata Made Faster and More Effective}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{47:1--47:17},
  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.47},
  URN =		{urn:nbn:de:0030-drops-132881},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.47},
  annote =	{Keywords: Updatable timed automata, Reachability, Zones, Simulations, Static analysis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.19
Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces

Authors: Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil

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

Abstract
We develop a new algebraic framework to reason about languages of Mazurkiewicz traces. This framework supports true concurrency and provides a non-trivial generalization of the wreath product operation to the trace setting. A novel local wreath product principle has been established. The new framework is crucially used to propose a decomposition result for recognizable trace languages, which is an analogue of the Krohn-Rhodes theorem. We prove this decomposition result in the special case of acyclic architectures and apply it to extend Kamp’s theorem to this setting. We also introduce and analyze distributed automata-theoretic operations called local and global cascade products. Finally, we show that aperiodic trace languages can be characterized using global cascade products of localized and distributed two-state reset automata.
Cite as

Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.CONCUR.2020.19,
  author =	{Adsul, Bharat and Gastin, Paul and Sarkar, Saptarshi and Weil, Pascal},
  title =	{{Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{19:1--19:17},
  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.19},
  URN =		{urn:nbn:de:0030-drops-128319},
  doi =		{10.4230/LIPIcs.CONCUR.2020.19},
  annote =	{Keywords: Mazurkiewicz traces, asynchronous automata, wreath product, cascade product, Krohn Rhodes decomposition theorem, local temporal logic over traces}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.29
Register Transducers Are Marble Transducers

Authors: Gaëtan Douéneau-Tabot, Emmanuel Filiot, and Paul Gastin

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
Deterministic two-way transducers define the class of regular functions from words to words. Alur and Cerný introduced an equivalent model of transducers with registers called copyless streaming string transducers. In this paper, we drop the "copyless" restriction on these machines and show that they are equivalent to two-way transducers enhanced with the ability to drop marks, named "marbles", on the input. We relate the maximal number of marbles used with the amount of register copies performed by the streaming string transducer. Finally, we show that the class membership problems associated with these models are decidable. Our results can be interpreted in terms of program optimization for simple recursive and iterative programs.
Cite as

Gaëtan Douéneau-Tabot, Emmanuel Filiot, and Paul Gastin. Register Transducers Are Marble Transducers. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 29:1-29:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{doueneautabot_et_al:LIPIcs.MFCS.2020.29,
  author =	{Dou\'{e}neau-Tabot, Ga\"{e}tan and Filiot, Emmanuel and Gastin, Paul},
  title =	{{Register Transducers Are Marble Transducers}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{29:1--29:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.29},
  URN =		{urn:nbn:de:0030-drops-126979},
  doi =		{10.4230/LIPIcs.MFCS.2020.29},
  annote =	{Keywords: streaming string transducer, two-way transducer, marbles, pebbles}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2019
LIPIcs, Volume 150, FSTTCS'19, Complete Volume

Authors: Arkadev Chattopadhyay and Paul Gastin

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
LIPIcs, Volume 150, FSTTCS'19, Complete Volume
Cite as

39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{chattopadhyay_et_al:LIPIcs.FSTTCS.2019,
  title =	{{LIPIcs, Volume 150, FSTTCS'19, Complete Volume}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019},
  URN =		{urn:nbn:de:0030-drops-116426},
  doi =		{10.4230/LIPIcs.FSTTCS.2019},
  annote =	{Keywords: Theory of computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSTTCS.2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Arkadev Chattopadhyay and Paul Gastin

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:LIPIcs.FSTTCS.2019.0,
  author =	{Chattopadhyay, Arkadev and Gastin, Paul},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{0:i--0:xii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.0},
  URN =		{urn:nbn:de:0030-drops-115621},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.76
Aperiodic Weighted Automata and Weighted First-Order Logic

Authors: Manfred Droste and Paul Gastin

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

Abstract
By fundamental results of Schützenberger, McNaughton and Papert from the 1970s, the classes of first-order definable and aperiodic languages coincide. Here, we extend this equivalence to a quantitative setting. For this, weighted automata form a general and widely studied model. We define a suitable notion of a weighted first-order logic. Then we show that this weighted first-order logic and aperiodic polynomially ambiguous weighted automata have the same expressive power. Moreover, we obtain such equivalence results for suitable weighted sublogics and finitely ambiguous or unambiguous aperiodic weighted automata. Our results hold for general weight structures, including all semirings, average computations of costs, bounded lattices, and others.
Cite as

Manfred Droste and Paul Gastin. Aperiodic Weighted Automata and Weighted First-Order Logic. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 76:1-76:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{droste_et_al:LIPIcs.MFCS.2019.76,
  author =	{Droste, Manfred and Gastin, Paul},
  title =	{{Aperiodic Weighted Automata and Weighted First-Order Logic}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{76:1--76:15},
  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.76},
  URN =		{urn:nbn:de:0030-drops-110203},
  doi =		{10.4230/LIPIcs.MFCS.2019.76},
  annote =	{Keywords: Weighted automata, weighted logic, aperiodic automata, first-order logic, unambiguous, finitely ambiguous, polynomially ambiguous}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.7
It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"

Authors: Benedikt Bollig, Marie Fortin, and Paul Gastin

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

Abstract
Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.
Cite as

Benedikt Bollig, Marie Fortin, and Paul Gastin. It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before". In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.CONCUR.2018.7,
  author =	{Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
  title =	{{It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{7:1--7:17},
  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.7},
  URN =		{urn:nbn:de:0030-drops-95455},
  doi =		{10.4230/LIPIcs.CONCUR.2018.7},
  annote =	{Keywords: communicating finite-state machines, first-order logic, happened-before relation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.28
Reachability in Timed Automata with Diagonal Constraints

Authors: Paul Gastin, Sayan Mukherjee, and B. Srivathsan

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

Abstract
We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in a data structure called "zones". Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice.
Cite as

Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in Timed Automata with Diagonal Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gastin_et_al:LIPIcs.CONCUR.2018.28,
  author =	{Gastin, Paul and Mukherjee, Sayan and Srivathsan, B.},
  title =	{{Reachability in Timed Automata with Diagonal Constraints}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{28:1--28:17},
  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.28},
  URN =		{urn:nbn:de:0030-drops-95660},
  doi =		{10.4230/LIPIcs.CONCUR.2018.28},
  annote =	{Keywords: Timed Automata, Reachability, Zones, Diagonal constraints}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.17
Communicating Finite-State Machines and Two-Variable Logic

Authors: Benedikt Bollig, Marie Fortin, and Paul Gastin

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.
Cite as

Benedikt Bollig, Marie Fortin, and Paul Gastin. Communicating Finite-State Machines and Two-Variable Logic. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.STACS.2018.17,
  author =	{Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
  title =	{{Communicating Finite-State Machines and Two-Variable Logic}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{17:1--17:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.17},
  URN =		{urn:nbn:de:0030-drops-85298},
  doi =		{10.4230/LIPIcs.STACS.2018.17},
  annote =	{Keywords: communicating finite-state machines, MSO logic, message sequence charts}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.39
Towards an Efficient Tree Automata Based Technique for Timed Systems

Authors: S. Akshay, Paul Gastin, Shankara Narayanan Krishna, and Ilias Sarkar

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.
Cite as

S. Akshay, Paul Gastin, Shankara Narayanan Krishna, and Ilias Sarkar. Towards an Efficient Tree Automata Based Technique for Timed Systems. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 39:1-39:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2017.39,
  author =	{Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Sarkar, Ilias},
  title =	{{Towards an Efficient Tree Automata Based Technique for Timed Systems}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{39:1--39:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.39},
  URN =		{urn:nbn:de:0030-drops-78017},
  doi =		{10.4230/LIPIcs.CONCUR.2017.39},
  annote =	{Keywords: Timed automata, tree automata, pushdown systems, tree-width}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.27
Analyzing Timed Systems Using Tree Automata

Authors: S. Akshay, Paul Gastin, and Shankara Narayanan Krishna

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

Abstract
Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. Such graphs can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).
Cite as

S. Akshay, Paul Gastin, and Shankara Narayanan Krishna. Analyzing Timed Systems Using Tree Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2016.27,
  author =	{Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan},
  title =	{{Analyzing Timed Systems Using Tree Automata}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{27:1--27:14},
  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.27},
  URN =		{urn:nbn:de:0030-drops-61775},
  doi =		{10.4230/LIPIcs.CONCUR.2016.27},
  annote =	{Keywords: Timed automata, tree automata, pushdown systems, tree-width}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.340
An Automata-Theoretic Approach to the Verification of Distributed Algorithms

Authors: Cyriac Aiswarya, Benedikt Bollig, and Paul Gastin

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

Abstract
We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete.
Cite as

Cyriac Aiswarya, Benedikt Bollig, and Paul Gastin. An Automata-Theoretic Approach to the Verification of Distributed Algorithms. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 340-353, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{aiswarya_et_al:LIPIcs.CONCUR.2015.340,
  author =	{Aiswarya, Cyriac and Bollig, Benedikt and Gastin, Paul},
  title =	{{An Automata-Theoretic Approach to the Verification of Distributed Algorithms}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{340--353},
  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.340},
  URN =		{urn:nbn:de:0030-drops-53737},
  doi =		{10.4230/LIPIcs.CONCUR.2015.340},
  annote =	{Keywords: distributed algorithms, verification, leader election}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2014.11
Reasoning About Distributed Systems: WYSIWYG (Invited Talk)

Authors: Aiswarya Cyriac and Paul Gastin

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

Abstract
There are two schools of thought on reasoning about distributed systems: one following interleaving based semantics, and one following partial-order/graph based semantics. This paper compares these two approaches and argues in favour of the latter. An introductory treatment of the split-width technique is also provided.
Cite as

Aiswarya Cyriac and Paul Gastin. Reasoning About Distributed Systems: WYSIWYG (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 11-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{cyriac_et_al:LIPIcs.FSTTCS.2014.11,
  author =	{Cyriac, Aiswarya and Gastin, Paul},
  title =	{{Reasoning About Distributed Systems: WYSIWYG}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{11--30},
  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.11},
  URN =		{urn:nbn:de:0030-drops-48283},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.11},
  annote =	{Keywords: Verification of distributed systems, Communicating recursive programs, Partial order/graph semantics, Split-width and tree interpretation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.625
Parameterized Communicating Automata: Complementation and Model Checking

Authors: Benedikt Bollig, Paul Gastin, and Akshay Kumar

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

Abstract
We study the language-theoretical aspects of parameterized communicating automata (PCAs), in which processes communicate via rendez-vous. A given PCA can be run on any topology of bounded degree such as pipelines, rings, ranked trees, and grids. We show that, under a context bound, which restricts the local behavior of each process, PCAs are effectively complementable. Complementability is considered a key aspect of robust automata models and can, in particular, be exploited for verification. In this paper, we use it to obtain a characterization of context-bounded PCAs in terms of monadic second-order (MSO) logic. As the emptiness problem for context-bounded PCAs is decidable for the classes of pipelines, rings, and trees, their model-checking problem wrt. MSO properties also becomes decidable. While previous work on model checking parameterized systems typically uses temporal logics without next operator, our MSO logic allows one to express several natural next modalities.
Cite as

Benedikt Bollig, Paul Gastin, and Akshay Kumar. Parameterized Communicating Automata: Complementation and Model Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 625-637, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.FSTTCS.2014.625,
  author =	{Bollig, Benedikt and Gastin, Paul and Kumar, Akshay},
  title =	{{Parameterized Communicating Automata: Complementation and Model Checking}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{625--637},
  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.625},
  URN =		{urn:nbn:de:0030-drops-48761},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.625},
  annote =	{Keywords: parameterized verification, complementation, monadic second-order logic}
}
Document
DOI: 10.4230/DagRep.4.1.104
Quantitative Models: Expressiveness, Analysis, and New Applications (Dagstuhl Seminar 14041)

Authors: Manfred Droste, Paul Gastin, Kim Gulstrand Larsen, and Axel Legay

Published in: Dagstuhl Reports, Volume 4, Issue 1 (2014)

Abstract
From Jan. 19 to Jan. 24, 2014, "Quantitative Models: Expressiveness, Analysis, and New Applications" was held in Schloss Dagstuhl-Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Manfred Droste, Paul Gastin, Kim Gulstrand Larsen, and Axel Legay. Quantitative Models: Expressiveness, Analysis, and New Applications (Dagstuhl Seminar 14041). In Dagstuhl Reports, Volume 4, Issue 1, pp. 104-124, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{droste_et_al:DagRep.4.1.104,
  author =	{Droste, Manfred and Gastin, Paul and Larsen, Kim Gulstrand and Legay, Axel},
  title =	{{Quantitative Models: Expressiveness, Analysis, and New Applications (Dagstuhl Seminar 14041)}},
  pages =	{104--124},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{1},
  editor =	{Droste, Manfred and Gastin, Paul and Larsen, Kim Gulstrand and Legay, Axel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.1.104},
  URN =		{urn:nbn:de:0030-drops-45374},
  doi =		{10.4230/DagRep.4.1.104},
  annote =	{Keywords: quantitative models, quantitative analysis, timed and hybrid systems, probabilistic systems, weighted automata, systems biology, smart grid}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.204
Model checking time-constrained scenario-based specifications

Authors: S. Akshay, Paul Gastin, Madhavan Mukund, and K. Narayan Kumar

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
We consider the problem of model checking message-passing systems with real-time requirements. As behavioural specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behaviour can be regarded as a timed automaton. Our goal is to verify that all timed behaviours exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking problem.
Cite as

S. Akshay, Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. Model checking time-constrained scenario-based specifications. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 204-215, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.FSTTCS.2010.204,
  author =	{Akshay, S. and Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
  title =	{{Model checking time-constrained scenario-based specifications}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{204--215},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.204},
  URN =		{urn:nbn:de:0030-drops-28649},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.204},
  annote =	{Keywords: model-checking, message-passing system, time-constrained MSC}
}
Document
DOI: 10.4230/DagSemProc.10031.1
10031 Abstracts Collection – Quantitative Models: Expressiveness and Analysis

Authors: Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen

Published in: Dagstuhl Seminar Proceedings, Volume 10031, Quantitative Models: Expressiveness and Analysis (2010)

Abstract
From Jan 18 to Jan 22, 2010, the Dagstuhl Seminar 10031 ``Quantitative Models: Expressiveness and Analysis '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen. 10031 Abstracts Collection – Quantitative Models: Expressiveness and Analysis. In Quantitative Models: Expressiveness and Analysis. Dagstuhl Seminar Proceedings, Volume 10031, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:DagSemProc.10031.1,
  author =	{Baier, Christel and Droste, Manfred and Gastin, Paul and Larsen, Kim Guldstrand},
  title =	{{10031 Abstracts Collection – Quantitative Models: Expressiveness and Analysis}},
  booktitle =	{Quantitative Models: Expressiveness and Analysis},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10031},
  editor =	{Christel Baier and Manfred Droste and Paul Gastin and Kim Guldstrand Larsen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10031.1},
  URN =		{urn:nbn:de:0030-drops-26839},
  doi =		{10.4230/DagSemProc.10031.1},
  annote =	{Keywords: Quantitative models, quantitative analysis, timed and hybrid systems, probabilistic systems, weighted automata}
}
Document
DOI: 10.4230/DagSemProc.10031.2
10031 Executive Summary – Quantitative Models: Expressiveness and Analysis

Authors: Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen

Published in: Dagstuhl Seminar Proceedings, Volume 10031, Quantitative Models: Expressiveness and Analysis (2010)

Abstract
Quantitative models and quantitative analysis in Computer Science are currently intensively studied, resulting in a revision of the foundation of Computer Science where classical yes/no answers are replaced by quantitative analyses. The potential application areas are huge, e.g., performance analysis, operational research or embedded systems. The aim of the seminar was to address three fundamental topics which are closely related: quantitative analysis of real-time and hybrid systems; probabilistic analysis and stochastic automata; weighted automata. These three areas of research have mainly evolved independently so far and the relationship between them has emerged only recently. The seminar brought together leading researchers of the three areas, with the goal of future highly productive cross-fertilizations.
Cite as

Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen. 10031 Executive Summary – Quantitative Models: Expressiveness and Analysis. In Quantitative Models: Expressiveness and Analysis. Dagstuhl Seminar Proceedings, Volume 10031, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:DagSemProc.10031.2,
  author =	{Baier, Christel and Droste, Manfred and Gastin, Paul and Larsen, Kim Guldstrand},
  title =	{{10031 Executive Summary – Quantitative Models: Expressiveness and Analysis}},
  booktitle =	{Quantitative Models: Expressiveness and Analysis},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10031},
  editor =	{Christel Baier and Manfred Droste and Paul Gastin and Kim Guldstrand Larsen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10031.2},
  URN =		{urn:nbn:de:0030-drops-26824},
  doi =		{10.4230/DagSemProc.10031.2},
  annote =	{Keywords: Quantitative models, quantitative analysis, timed and hybrid systems, probabilistic systems, weighted automata}
}
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