15 Search Results for "Finkel, Alain"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.16
Acyclic Petri and Workflow Nets with Resets

Authors: Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, and Henry Sinclair-Banks

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

Abstract
In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition that only applies to the consumptions and productions, not the resets. The first class is acyclic Petri nets with resets, and we show that coverability is PSPACE-complete for them. This contrasts the known Ackermann-hardness for coverability in (not necessarily acyclic) Petri nets with resets. We prove that the reachability problem remains undecidable for acyclic Petri nets with resets. The second class concerns workflow nets, a practically motivated and natural subclass of Petri nets. Here, we show that both coverability and reachability in acyclic workflow nets with resets are PSPACE-complete. Without the acyclicity condition, reachability and coverability in workflow nets with resets are known to be equally hard as for Petri nets with resets, that being Ackermann-hard and undecidable, respectively.
Cite as

Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, and Henry Sinclair-Banks. Acyclic Petri and Workflow Nets with Resets. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.FSTTCS.2023.16,
  author =	{Chistikov, Dmitry and Czerwi\'{n}ski, Wojciech and Hofman, Piotr and Mazowiecki, Filip and Sinclair-Banks, Henry},
  title =	{{Acyclic Petri and Workflow Nets with Resets}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.16},
  URN =		{urn:nbn:de:0030-drops-193892},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.16},
  annote =	{Keywords: Petri nets, Workflow Nets, Resets, Acyclic, Reachability, Coverability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.42
Counter Machines with Infrequent Reversals

Authors: Alain Finkel, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Georg Zetzsche

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

Abstract
Bounding the number of reversals in a counter machine is one of the most prominent restrictions to achieve decidability of the reachability problem. Given this success, we explore whether this notion can be relaxed while retaining decidability. To this end, we introduce the notion of an f-reversal-bounded counter machine for a monotone function f: ℕ → ℕ. In such a machine, every run of length n makes at most f(n) reversals. Our first main result is a dichotomy theorem: We show that for every monotone function f, one of the following holds: Either (i) f grows so slowly that every f-reversal bounded counter machine is already k-reversal bounded for some constant k or (ii) f belongs to Ω(log(n)) and reachability in f-reversal bounded counter machines is undecidable. This shows that classical reversal bounding already captures the decidable cases of f-reversal bounding for any monotone function f. The key technical ingredient is an analysis of the growth of small solutions of iterated compositions of Presburger-definable constraints. In our second contribution, we investigate whether imposing f-reversal boundedness improves the complexity of the reachability problem in vector addition systems with states (VASS). Here, we obtain an analogous dichotomy: We show that either (i) f grows so slowly that every f-reversal-bounded VASS is already k-reversal-bounded for some constant k or (ii) f belongs to Ω(n) and the reachability problem for f-reversal-bounded VASS remains Ackermann-complete. This result is proven using run amalgamation in VASS. Overall, our results imply that classical restriction of reversal boundedness is a robust one.
Cite as

Alain Finkel, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Georg Zetzsche. Counter Machines with Infrequent Reversals. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2023.42,
  author =	{Finkel, Alain and Krishna, Shankara Narayanan and Madnani, Khushraj and Majumdar, Rupak and Zetzsche, Georg},
  title =	{{Counter Machines with Infrequent Reversals}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{42:1--42:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.42},
  URN =		{urn:nbn:de:0030-drops-194152},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.42},
  annote =	{Keywords: Counter machines, reversal-bounded, reachability, decidability, complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.14
About Decisiveness of Dynamic Probabilistic Models

Authors: Alain Finkel, Serge Haddad, and Lina Ye

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

Abstract
Decisiveness of infinite Markov chains with respect to some (finite or infinite) target set of states is a key property that allows to compute the reachability probability of this set up to an arbitrary precision. Most of the existing works assume constant weights for defining the probability of a transition in the considered models. However numerous probabilistic modelings require the (dynamic) weight to also depend on the current state. So we introduce a dynamic probabilistic version of counter machine (pCM). After establishing that decisiveness is undecidable for pCMs even with constant weights, we study the decidability of decisiveness for subclasses of pCM. We show that, without restrictions on dynamic weights, decisiveness is undecidable with a single state and single counter pCM. On the contrary with polynomial weights, decisiveness becomes decidable for single counter pCMs under mild conditions. Then we show that decisiveness of probabilistic Petri nets (pPNs) with polynomial weights is undecidable even when the target set is upward-closed unlike the case of constant weights. Finally we prove that the standard subclass of pPNs with a regular language is decisive with respect to a finite set whatever the kind of weights.
Cite as

Alain Finkel, Serge Haddad, and Lina Ye. About Decisiveness of Dynamic Probabilistic Models. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.CONCUR.2023.14,
  author =	{Finkel, Alain and Haddad, Serge and Ye, Lina},
  title =	{{About Decisiveness of Dynamic Probabilistic Models}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{14:1--14: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.14},
  URN =		{urn:nbn:de:0030-drops-190089},
  doi =		{10.4230/LIPIcs.CONCUR.2023.14},
  annote =	{Keywords: infinite Markov chain, reachability probability, decisiveness}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.14
A Unifying Framework for Deciding Synchronizability

Authors: Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Several notions of synchronizability of a message-passing system have been introduced in the literature. Roughly, a system is called synchronizable if every execution can be rescheduled so that it meets certain criteria, e.g., a channel bound. We provide a framework, based on MSO logic and (special) tree-width, that unifies existing definitions, explains their good properties, and allows one to easily derive other, more general definitions and decidability results for synchronizability.
Cite as

Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh. A Unifying Framework for Deciding Synchronizability. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.CONCUR.2021.14,
  author =	{Bollig, Benedikt and Di Giusto, Cinzia and Finkel, Alain and Laversa, Laetitia and Lozes, Etienne and Suresh, Amrita},
  title =	{{A Unifying Framework for Deciding Synchronizability}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.14},
  URN =		{urn:nbn:de:0030-drops-143917},
  doi =		{10.4230/LIPIcs.CONCUR.2021.14},
  annote =	{Keywords: communicating finite-state machines, message sequence charts, synchronizability, MSO logic, special tree-width}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.49
Bounded Reachability Problems Are Decidable in FIFO Machines

Authors: Benedikt Bollig, Alain Finkel, and Amrita Suresh

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

Abstract
The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular channel belongs to a given bounded language). We prove, by reducing this model to a counter machine with restricted zero tests, that the rational-reachability problem (and by extension, control-state reachability, unboundedness, deadlock, etc.) is decidable. This class of machines subsumes input-letter-bounded machines, flat machines, linear FIFO nets, and monogeneous machines, for which some of these problems were already shown to be decidable. These theoretical results can form the foundations to build a tool to verify general FIFO machines based on the analysis of input-bounded machines.
Cite as

Benedikt Bollig, Alain Finkel, and Amrita Suresh. Bounded Reachability Problems Are Decidable in FIFO Machines. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 49:1-49:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.CONCUR.2020.49,
  author =	{Bollig, Benedikt and Finkel, Alain and Suresh, Amrita},
  title =	{{Bounded Reachability Problems Are Decidable in FIFO Machines}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{49:1--49: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.49},
  URN =		{urn:nbn:de:0030-drops-128615},
  doi =		{10.4230/LIPIcs.CONCUR.2020.49},
  annote =	{Keywords: FIFO machines, reachability, underapproximation, counter machines}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2019.3
Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk)

Authors: Ranko Lazić

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

Abstract
Studying one-dimensional grammar vector addition systems has long been advocated by Alain Finkel. In this presentation, we shall see how research on those systems has led to the recent breakthrough tower lower bound for the reachability problem on vector addition systems, obtained by Czerwiński et al. In fact, we shall look at how appropriate modifications of an underlying technical construction can lead to counter-examples to several conjectures on one-dimensional grammar vector addition systems, fixed-dimensional vector addition systems, and fixed-dimensional flat vector addition systems.
Cite as

Ranko Lazić. Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk). In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lazic:LIPIcs.FSTTCS.2019.3,
  author =	{Lazi\'{c}, Ranko},
  title =	{{Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{3:1--3:2},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.3},
  URN =		{urn:nbn:de:0030-drops-115653},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.3},
  annote =	{Keywords: Petri nets, vector addition systems, reachability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.41
The Well Structured Problem for Presburger Counter Machines

Authors: Alain Finkel and Ekanshdeep Gupta

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

Abstract
We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.
Cite as

Alain Finkel and Ekanshdeep Gupta. The Well Structured Problem for Presburger Counter Machines. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 41:1-41:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2019.41,
  author =	{Finkel, Alain and Gupta, Ekanshdeep},
  title =	{{The Well Structured Problem for Presburger Counter Machines}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{41:1--41:15},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.41},
  URN =		{urn:nbn:de:0030-drops-116037},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.41},
  annote =	{Keywords: Well structured transition systems, infinite state systems, Presburger counter machines, reachability, coverability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.12
Verification of Flat FIFO Systems

Authors: Alain Finkel and M. Praveen

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

Abstract
The decidability and complexity of reachability problems and model-checking for flat counter systems have been explored in detail. However, only few results are known for flat FIFO systems, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO systems, generalizing similar existing results for flat counter systems. We construct a trace-flattable counter system that is bisimilar to a given flat FIFO system, which allows to model-check the original flat FIFO system. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO systems based on analysis of flat subsystems.
Cite as

Alain Finkel and M. Praveen. Verification of Flat FIFO Systems. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.CONCUR.2019.12,
  author =	{Finkel, Alain and Praveen, M.},
  title =	{{Verification of Flat FIFO Systems}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{12:1--12:17},
  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.12},
  URN =		{urn:nbn:de:0030-drops-109147},
  doi =		{10.4230/LIPIcs.CONCUR.2019.12},
  annote =	{Keywords: Infinite state systems, FIFO, counters, flat systems, reachability, termination, complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.31
Reachability for Two-Counter Machines with One Test and One Reset

Authors: Alain Finkel, Jérôme Leroux, and Grégoire Sutre

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.
Cite as

Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for Two-Counter Machines with One Test and One Reset. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2018.31,
  author =	{Finkel, Alain and Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
  title =	{{Reachability for Two-Counter Machines with One Test and One Reset}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{31:1--31:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.31},
  URN =		{urn:nbn:de:0030-drops-99305},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.31},
  annote =	{Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Presburger arithmetic, Infinite-state system}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.16
Forward Analysis for WSTS, Part III: Karp-Miller Trees

Authors: Michael Blondin, Alain Finkel, and Jean Goubault-Larrecq

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
This paper is a sequel of "Forward Analysis for WSTS, Part I: Completions" [STACS 2009, LZI Intl. Proc. in Informatics 3, 433–444] and "Forward Analysis for WSTS, Part II: Complete WSTS" [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downwards-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural assumptions on positive sequences, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.
Cite as

Michael Blondin, Alain Finkel, and Jean Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.FSTTCS.2017.16,
  author =	{Blondin, Michael and Finkel, Alain and Goubault-Larrecq, Jean},
  title =	{{Forward Analysis for WSTS, Part III: Karp-Miller Trees}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{16:1--16:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.16},
  URN =		{urn:nbn:de:0030-drops-84033},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.16},
  annote =	{Keywords: WSTS, model checking, coverability, Karp-Miller algorithm, ideals}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.122
Synchronizability of Communicating Finite State Machines is not Decidable

Authors: Alain Finkel and Etienne Lozes

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

Abstract
A system of communicating finite state machines is synchronizable if its send trace semantics, i.e. the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thanks to a form of small model property. In this paper, we show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We close this question for peer-to-peer communications, and we show that synchronizability is actually undecidable. We show that synchronizability is decidable if the topology of communications is an oriented ring. We also show that, in this case, synchronizability implies the absence of unspecified receptions and orphan messages, and the channel-recognizability of the reachability set.
Cite as

Alain Finkel and Etienne Lozes. Synchronizability of Communicating Finite State Machines is not Decidable. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 122:1-122:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.ICALP.2017.122,
  author =	{Finkel, Alain and Lozes, Etienne},
  title =	{{Synchronizability of Communicating Finite State Machines is not Decidable}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{122:1--122:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.122},
  URN =		{urn:nbn:de:0030-drops-74020},
  doi =		{10.4230/LIPIcs.ICALP.2017.122},
  annote =	{Keywords: verification, distributed system, asynchronous communications, choreographies}
}
Document
DOI: 10.4230/DagRep.4.3.153
Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141)

Authors: Javier Esparza, Alain Finkel, Pierre McKenzie, and Joel Ouaknine

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

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14141 "Reachability Problems for Infinite-State Systems", held from March 30th until April 4th, 2014. The seminar gathered 44 participants and the program consisted of 34 presentations. Participants were asked to contribute open questions prior and during the seminar. A list of these open questions appears in a separate section of the present report. This list generated collaborations among participants and gave rise to research publications solving (partially), for example, question 5.13, namely "what functions are computable by VASS?"
Cite as

Javier Esparza, Alain Finkel, Pierre McKenzie, and Joel Ouaknine. Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141). In Dagstuhl Reports, Volume 4, Issue 3, pp. 153-180, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{esparza_et_al:DagRep.4.3.153,
  author =	{Esparza, Javier and Finkel, Alain and McKenzie, Pierre and Ouaknine, Joel},
  title =	{{Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141)}},
  pages =	{153--180},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{3},
  editor =	{Esparza, Javier and Finkel, Alain and McKenzie, Pierre and Ouaknine, Joel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.3.153},
  URN =		{urn:nbn:de:0030-drops-46121},
  doi =		{10.4230/DagRep.4.3.153},
  annote =	{Keywords: Infinite-State Systems, Reachability Problems, Formal Verification, Well-Structured Transition Systems, Counter Machines, Vector Addition Systems, Timed Systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.301
Extending the Rackoff technique to Affine nets

Authors: Rémi Bonnet, Alain Finkel, and M. Praveen

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

Abstract
We study the possibility of extending the Rackoff technique to Affine nets, which are Petri nets extended with affine functions. The Rackoff technique has been used for establishing EXPSPACE upper bounds for the coverability and boundedness problems for Petri nets. We show that this technique can be extended to strongly increasing Affine nets, obtaining better upper bounds compared to known results. The possible copies between places of a strongly increasing Affine net make this extension non-trivial. One cannot expect similar results for the entire class of Affine nets since coverability is Ackermann-hard and boundedness is undecidable. Moreover, it can be proved that model checking a logic expressing generalized coverability properties is undecidable for strongly increasing Affine nets, while it is known to be EXPSPACE-complete for Petri nets.
Cite as

Rémi Bonnet, Alain Finkel, and M. Praveen. Extending the Rackoff technique to Affine nets. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 301-312, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bonnet_et_al:LIPIcs.FSTTCS.2012.301,
  author =	{Bonnet, R\'{e}mi and Finkel, Alain and Praveen, M.},
  title =	{{Extending the Rackoff technique to Affine nets}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{301--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.301},
  URN =		{urn:nbn:de:0030-drops-38688},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.301},
  annote =	{Keywords: Complexity of VASS, Affine nets, Rackoff technique, model checking, coverability, boundedness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.192
Place-Boundedness for Vector Addition Systems with one zero-test

Authors: Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun

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

Abstract
Reachability and boundedness problems have been shown decidable for Vector Addition Systems with one zero-test. Surprisingly, place-boundedness remained open. We provide here a variation of the Karp-Miller algorithm to compute a basis of the downward closure of the reachability set which allows to decide place-boundedness. This forward algorithm is able to pass the zero-tests thanks to a finer cover, hybrid between the reachability and cover sets, reclaiming accuracy on one component. We show that this filtered cover is still recursive, but that equality of two such filtered covers, even for usual Vector Addition Systems (with no zero-test), is undecidable.
Cite as

Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Place-Boundedness for Vector Addition Systems with one zero-test. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 192-203, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bonnet_et_al:LIPIcs.FSTTCS.2010.192,
  author =	{Bonnet, R\'{e}mi and Finkel, Alain and Leroux, J\'{e}r\^{o}me and Zeitoun, Marc},
  title =	{{Place-Boundedness for Vector Addition Systems with one zero-test}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{192--203},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.192},
  URN =		{urn:nbn:de:0030-drops-28638},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.192},
  annote =	{Keywords: Place-boundedness, vector addition system with one zero-test, Karp-Miller algorithm}
}
Document
DOI: 10.4230/LIPIcs.STACS.2009.1844
Forward Analysis for WSTS, Part I: Completions

Authors: Alain Finkel and Jean Goubault-Larrecq

Published in: LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

Abstract
Well-structured transition systems provide the right foundation to compute a finite basis of the set of predecessors of the upward closure of a state. The dual problem, to compute a finite representation of the set of successors of the downward closure of a state, is harder: Until now, the theoretical framework for manipulating downward-closed sets was missing. We answer this problem, using insights from domain theory (dcpos and ideal completions), from topology (sobrifications), and shed new light on the notion of adequate domains of limits.
Cite as

Alain Finkel and Jean Goubault-Larrecq. Forward Analysis for WSTS, Part I: Completions. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 433-444, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.STACS.2009.1844,
  author =	{Finkel, Alain and Goubault-Larrecq, Jean},
  title =	{{Forward Analysis for WSTS, Part I: Completions}},
  booktitle =	{26th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{433--444},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-09-5},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{3},
  editor =	{Albers, Susanne and Marion, Jean-Yves},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1844},
  URN =		{urn:nbn:de:0030-drops-18444},
  doi =		{10.4230/LIPIcs.STACS.2009.1844},
  annote =	{Keywords: WSTS, Forward analysis, Completion, Karp-Miller procedure, Domain theory, Sober spaces, Noetherian spaces}
}
  • Refine by Author
  • 13 Finkel, Alain
  • 2 Bollig, Benedikt
  • 2 Bonnet, Rémi
  • 2 Goubault-Larrecq, Jean
  • 2 Leroux, Jérôme
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Concurrency
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Models of computation
  • 2 Theory of computation → Verification by model checking
  • 1 Mathematics of computing → Markov processes
  • Show More...

  • Refine by Keyword
  • 5 reachability
  • 3 coverability
  • 2 Karp-Miller algorithm
  • 2 Petri nets
  • 2 WSTS
  • Show More...

  • Refine by Type
  • 15 document

  • Refine by Publication Year
  • 3 2019
  • 3 2023
  • 2 2018
  • 1 2009
  • 1 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