21 Search Results for "Walukiewicz, Igor"

Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2023.1
CONCUR Test-Of-Time Award 2023 (Invited Paper)

Authors: Bengt Jonsson, Marta Kwiatkowska, and Igor Walukiewicz

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

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

Bengt Jonsson, Marta Kwiatkowska, and Igor Walukiewicz. CONCUR Test-Of-Time Award 2023 (Invited Paper). In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:LIPIcs.CONCUR.2023.1,
  author =	{Jonsson, Bengt and Kwiatkowska, Marta and Walukiewicz, Igor},
  title =	{{CONCUR Test-Of-Time Award 2023}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.1},
  URN =		{urn:nbn:de:0030-drops-189953},
  doi =		{10.4230/LIPIcs.CONCUR.2023.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.24
Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints

Authors: Corto Mascle, Anca Muscholl, and Igor Walukiewicz

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verification problem is to determine if a given system has a limit configuration satisfying a given regular property. This formulation of the problem encompasses verification of reachability as well as of many liveness properties. We show that this verification problem, while undecidable in general, is decidable for nested lock usage. We show Exptime-completeness of the verification problem. The main source of complexity is the number of parameters in the spawn operation. If the number of parameters is bounded, our algorithm works in Ptime for properties expressed by parity automata with a fixed number of ranks.
Cite as

Corto Mascle, Anca Muscholl, and Igor Walukiewicz. Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mascle_et_al:LIPIcs.CONCUR.2023.24,
  author =	{Mascle, Corto and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.24},
  URN =		{urn:nbn:de:0030-drops-190184},
  doi =		{10.4230/LIPIcs.CONCUR.2023.24},
  annote =	{Keywords: Parametric systems, Locks, Model-checking}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.118
How to Play Optimally for Regular Objectives?

Authors: Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
This paper studies two-player zero-sum games played on graphs and makes contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of one of the two players is that eventually the sequence of colors along the play belongs to some regular language of finite words. We obtain different characterizations of the chromatic memory requirements for such objectives for both players, from which we derive complexity-theoretic statements: deciding whether there exist small memory structures sufficient to play optimally is NP-complete for both players. Some of our characterization results apply to a more general class of objectives: topologically closed and topologically open sets.
Cite as

Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove. How to Play Optimally for Regular Objectives?. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 118:1-118:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.ICALP.2023.118,
  author =	{Bouyer, Patricia and Fijalkow, Nathana\"{e}l and Randour, Mickael and Vandenhove, Pierre},
  title =	{{How to Play Optimally for Regular Objectives?}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{118:1--118:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.118},
  URN =		{urn:nbn:de:0030-drops-181700},
  doi =		{10.4230/LIPIcs.ICALP.2023.118},
  annote =	{Keywords: two-player games on graphs, strategy complexity, regular languages, finite-memory strategies, NP-completeness}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.12
Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics

Authors: Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz

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

Abstract
We study the Büchi non-emptiness problem for networks of timed automata. Standard solutions consider the network as a monolithic timed automaton obtained as a synchronized product and build its zone graph on-the-fly under the classical global-time semantics. In the global-time semantics, all processes are assumed to have a common global timeline. Bengtsson et al. in 1998 have proposed a local-time semantics where each process in the network moves independently according to a local timeline, and processes synchronize their timelines when they do a common action. It has been shown that the local-time semantics is equivalent to the global-time semantics for finite runs, and hence can be used for checking reachability. The local-time semantics allows computation of a local zone graph which has good independence properties and is amenable to partial-order methods. Hence local zone graphs are able to better tackle the state-space explosion due to concurrency. In this work, we extend the results to the Büchi setting. We propose a local zone graph computation that can be coupled with a partial-order method, to solve the Büchi non-emptiness problem in timed networks. In the process, we develop a theory of regions for the local-time semantics.
Cite as

Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 12:1-12:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.CONCUR.2022.12,
  author =	{Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Walukiewicz, Igor},
  title =	{{Checking Timed B\"{u}chi Automata Emptiness Using the Local-Time Semantics}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{12:1--12:24},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.12},
  URN =		{urn:nbn:de:0030-drops-170756},
  doi =		{10.4230/LIPIcs.CONCUR.2022.12},
  annote =	{Keywords: Timed B\"{u}chi automata, local-time semantics, zones, abstraction, partial-order reduction}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.20
Half-Positional Objectives Recognized by Deterministic Büchi Automata

Authors: Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove

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

Abstract
A central question in the theory of two-player games over graphs is to understand which objectives are half-positional, that is, which are the objectives for which the protagonist does not need memory to implement winning strategies. Objectives for which both players do not need memory have already been characterized (both in finite and infinite graphs); however, less is known about half-positional objectives. In particular, no characterization of half-positionality is known for the central class of ω-regular objectives. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, in both finite and infinite graphs. Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
Cite as

Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-Positional Objectives Recognized by Deterministic Büchi Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2022.20,
  author =	{Bouyer, Patricia and Casares, Antonio and Randour, Mickael and Vandenhove, Pierre},
  title =	{{Half-Positional Objectives Recognized by Deterministic B\"{u}chi Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{20:1--20: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.20},
  URN =		{urn:nbn:de:0030-drops-170833},
  doi =		{10.4230/LIPIcs.CONCUR.2022.20},
  annote =	{Keywords: two-player games on graphs, half-positionality, memoryless optimal strategies, B\"{u}chi automata, \omega-regularity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.125
Distributed Controller Synthesis for Deadlock Avoidance

Authors: Hugo Gimbert, Corto Mascle, Anca Muscholl, and Igor Walukiewicz

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two locks. The problem then becomes complete for the second level of the polynomial time hierarchy, and even in Ptime under some additional assumptions. The dining philosophers problem satisfies these assumptions. The second restriction is a nested usage of locks. In this case the synthesis problem is Nexptime-complete. The drinking philosophers problem falls in this case.
Cite as

Hugo Gimbert, Corto Mascle, Anca Muscholl, and Igor Walukiewicz. Distributed Controller Synthesis for Deadlock Avoidance. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 125:1-125:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gimbert_et_al:LIPIcs.ICALP.2022.125,
  author =	{Gimbert, Hugo and Mascle, Corto and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Distributed Controller Synthesis for Deadlock Avoidance}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{125:1--125:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.125},
  URN =		{urn:nbn:de:0030-drops-164668},
  doi =		{10.4230/LIPIcs.ICALP.2022.125},
  annote =	{Keywords: Distributed Synthesis, Concurrency, Lock Synchronisation, Deadlock Avoidance}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.12
On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions

Authors: Antonio Casares

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

Abstract
In this paper, we relate the problem of determining the chromatic memory requirements of Muller conditions with the minimisation of transition-based Rabin automata. Our first contribution is a proof of the NP-completeness of the minimisation of transition-based Rabin automata. Our second contribution concerns the memory requirements of games over graphs using Muller conditions. A memory structure is a finite state machine that implements a strategy and is updated after reading the edges of the game; the special case of chromatic memories being those structures whose update function only consider the colours of the edges. We prove that the minimal amount of chromatic memory required in games using a given Muller condition is exactly the size of a minimal Rabin automaton recognising this condition. Combining these two results, we deduce that finding the chromatic memory requirements of a Muller condition is NP-complete. This characterisation also allows us to prove that chromatic memories cannot be optimal in general, disproving a conjecture by Kopczyński.
Cite as

Antonio Casares. On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{casares:LIPIcs.CSL.2022.12,
  author =	{Casares, Antonio},
  title =	{{On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{12:1--12: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.12},
  URN =		{urn:nbn:de:0030-drops-157322},
  doi =		{10.4230/LIPIcs.CSL.2022.12},
  annote =	{Keywords: Automata on Infinite Words, Games on Graphs, Arena-Independent Memory, Complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.9
Characterizing Consensus in the Heard-Of Model

Authors: A. R. Balasubramanian and Igor Walukiewicz

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

Abstract
The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm.
Cite as

A. R. Balasubramanian and Igor Walukiewicz. Characterizing Consensus in the Heard-Of Model. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{balasubramanian_et_al:LIPIcs.CONCUR.2020.9,
  author =	{Balasubramanian, A. R. and Walukiewicz, Igor},
  title =	{{Characterizing Consensus in the Heard-Of Model}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{9:1--9:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.9},
  URN =		{urn:nbn:de:0030-drops-128217},
  doi =		{10.4230/LIPIcs.CONCUR.2020.9},
  annote =	{Keywords: consensus problem, Heard-Of model, verification}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.10
Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time

Authors: Paweł Parys

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

Abstract
Calude, Jain, Khoussainov, Li, and Stephan (2017) proposed a quasi-polynomial-time algorithm solving parity games. After this breakthrough result, a few other quasi-polynomial-time algorithms were introduced; none of them is easy to understand. Moreover, it turns out that in practice they operate very slowly. On the other side there is Zielonka’s recursive algorithm, which is very simple, exponential in the worst case, and the fastest in practice. We combine these two approaches: we propose a small modification of Zielonka’s algorithm, which ensures that the running time is at most quasi-polynomial. In effect, we obtain a simple algorithm that solves parity games in quasi-polynomial time. We also hope that our algorithm, after further optimizations, can lead to an algorithm that shares the good performance of Zielonka’s algorithm on typical inputs, while reducing the worst-case complexity on difficult inputs.
Cite as

Paweł Parys. Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 10:1-10:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.MFCS.2019.10,
  author =	{Parys, Pawe{\l}},
  title =	{{Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{10:1--10: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.10},
  URN =		{urn:nbn:de:0030-drops-109543},
  doi =		{10.4230/LIPIcs.MFCS.2019.10},
  annote =	{Keywords: Parity games, Zielonka’s algorithm, quasi-polynomial time}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.16
Revisiting Local Time Semantics for Networks of Timed Automata

Authors: R. Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz

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

Abstract
We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion is particularly visible as even different interleavings of local actions of processes may lead to different zones. Salah et al. in 2006 have shown that the union of all these different zones is also a zone. This observation was used in an algorithm which from time to time detects and aggregates these zones into a single zone. We show that such aggregated zones can be calculated more efficiently using the local time semantics and the related notion of local zones proposed by Bengtsson et al. in 1998. Next, we point out a flaw in the existing method to ensure termination of the local zone graph computation. We fix this with a new algorithm that builds the local zone graph and uses abstraction techniques over (standard) zones for termination. We evaluate our algorithm on standard examples. On various examples, we observe an order of magnitude decrease in the search space. On the other examples, the algorithm performs like the standard zone algorithm.
Cite as

R. Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Revisiting Local Time Semantics for Networks of Timed Automata. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{govind_et_al:LIPIcs.CONCUR.2019.16,
  author =	{Govind, R. and Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Walukiewicz, Igor},
  title =	{{Revisiting Local Time Semantics for Networks of Timed Automata}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{16:1--16: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.16},
  URN =		{urn:nbn:de:0030-drops-109184},
  doi =		{10.4230/LIPIcs.CONCUR.2019.16},
  annote =	{Keywords: Timed automata, verification, local-time semantics, abstraction}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.48
Why Liveness for Timed Automata Is Hard, and What We Can Do About It

Authors: Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
The liveness problem for timed automata asks if a given automaton has a run passing infinitely often through an accepting state. We show that unless P=NP, the liveness problem is more difficult than the reachability problem; more precisely, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is NP-hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it with the existing solutions.
Cite as

Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. Why Liveness for Timed Automata Is Hard, and What We Can Do About It. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 48:1-48:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.FSTTCS.2016.48,
  author =	{Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Tran, Thanh-Tung and Walukiewicz, Igor},
  title =	{{Why Liveness for Timed Automata Is Hard, and What We Can Do About It}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{48:1--48:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.48},
  URN =		{urn:nbn:de:0030-drops-68831},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.48},
  annote =	{Keywords: Timed automata, model-checking, liveness invariant, state subsumption}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.12
Soundness in Negotiations

Authors: Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz

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

Abstract
Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In a former paper, Esparza and Desel have shown that deciding soundness of a negotiation is PSPACE-complete, and in PTIME if the negotiation is deterministic. They have also provided an algorithm for an intermediate class of acyclic, non-deterministic negotiations, but left the complexity of the soundness problem open. In the first part of this paper we study two further analysis problems for sound acyclic deterministic negotiations, called the race and the omission problem, and give polynomial algorithms. We use these results to provide the first polynomial algorithm for some analysis problems of workflow nets with data previously studied by Trcka, van der Aalst, and Sidorova. In the second part we solve the open question of Esparza and Desel's paper. We show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.
Cite as

Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz. Soundness in Negotiations. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 12:1-12:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2016.12,
  author =	{Esparza, Javier and Kuperberg, Denis and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Soundness in Negotiations}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{12:1--12:13},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.12},
  URN =		{urn:nbn:de:0030-drops-61636},
  doi =		{10.4230/LIPIcs.CONCUR.2016.12},
  annote =	{Keywords: Negotiations, workflows, soundness, verification, concurrency}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.99
Deciding the Topological Complexity of Büchi Languages

Authors: Michal Skrzypczak and Igor Walukiewicz

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We study the topological complexity of languages of Büchi automata on infinite binary trees. We show that such a language is either Borel and WMSO-definable, or Sigma_1^1-complete and not WMSO-definable; moreover it can be algorithmically decided which of the two cases holds. The proof relies on a direct reduction to deciding the winner in a finite game with a regular winning condition.
Cite as

Michal Skrzypczak and Igor Walukiewicz. Deciding the Topological Complexity of Büchi Languages. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 99:1-99:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{skrzypczak_et_al:LIPIcs.ICALP.2016.99,
  author =	{Skrzypczak, Michal and Walukiewicz, Igor},
  title =	{{Deciding the Topological Complexity of B\"{u}chi Languages}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{99:1--99:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.99},
  URN =		{urn:nbn:de:0030-drops-62346},
  doi =		{10.4230/LIPIcs.ICALP.2016.99},
  annote =	{Keywords: tree automata, non-determinism, Borel sets, topological complexity, decidability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.163
Ordered Tree-Pushdown Systems

Authors: Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz

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

Abstract
We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application, we show that our simple model can encode several formalisms generalizing pushdown systems, such as ordered multi-pushdown systems, annotated higher-order pushdown systems, the Krivine machine, and ordered annotated multi-pushdown systems. In each case, our procedure yields tight complexity.
Cite as

Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered Tree-Pushdown Systems. 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. 163-177, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.FSTTCS.2015.163,
  author =	{Clemente, Lorenzo and Parys, Pawel and Salvati, Sylvain and Walukiewicz, Igor},
  title =	{{Ordered Tree-Pushdown Systems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{163--177},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.163},
  URN =		{urn:nbn:de:0030-drops-56470},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.163},
  annote =	{Keywords: reachability analysis, saturation technique, pushdown automata, ordered pushdown automata, higher-order pushdown automata, higher-order recursive sche}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.229
A Model for Behavioural Properties of Higher-order Programs

Authors: Sylvain Salvati and Igor Walukiewicz

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We consider simply typed lambda-calculus with fixpoints as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as a potentially infinite tree of calls to built-in operations. Properties of such trees are properties of executions of programs and monadic second-order logic (MSOL) is well suited to express them. For a given MSOL property we show how to construct a finitary model recognizing it. In other words, the value of a lambda-term in the model determines if the tree that is the result of the execution of the term satisfies the property. The finiteness of the construction has as consequences many known results about the verification of higher-order programs in this framework.
Cite as

Sylvain Salvati and Igor Walukiewicz. A Model for Behavioural Properties of Higher-order Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 229-243, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{salvati_et_al:LIPIcs.CSL.2015.229,
  author =	{Salvati, Sylvain and Walukiewicz, Igor},
  title =	{{A Model for Behavioural Properties of Higher-order Programs}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{229--243},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.229},
  URN =		{urn:nbn:de:0030-drops-54173},
  doi =		{10.4230/LIPIcs.CSL.2015.229},
  annote =	{Keywords: Simply typed lambda-Y-calculus, Monadic second order logic, semantic models}
}
  • Refine by Author
  • 17 Walukiewicz, Igor
  • 5 Muscholl, Anca
  • 4 Herbreteau, Frédéric
  • 4 Srivathsan, B.
  • 3 Salvati, Sylvain
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Distributed computing models
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Verification by model checking
  • 1 Software and its engineering → Software verification
  • 1 Theory of computation → Algorithmic game theory
  • Show More...

  • Refine by Keyword
  • 3 verification
  • 2 Game semantics
  • 2 Model checking
  • 2 Model-checking
  • 2 Semantics of programming languages
  • Show More...

  • Refine by Type
  • 21 document

  • Refine by Publication Year
  • 4 2022
  • 3 2015
  • 3 2016
  • 3 2023
  • 2 2010
  • Show More...

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