1 citations · 1 across the 9 of their papers we have counts for
12 papers
Representing One Letter Weighted Automata Over the Tropical Semiring
Shaull Almagor, Ismaël Jecker, Filip Mazowiecki +3
We consider weighted automata over the tropical semiring . Recently, it was shown that determinisation is decidable; in this paper we focus on the comple…
Reachability in VASS Extended with Integer Counters
Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg +5
We consider a variant of VASS extended with integer counters, denoted VASS+Z. These are automata equipped with N and Z counters; the N-counters are required to remain nonnegative a…
Exploring VASS Parameterised by Geometric Dimension
Wojciech Czerwiński, Roland Guttenberg, Łukasz Orlikowski +2
The geometric dimension of a Vector Addition System with States (VASS) is the dimension of the vector space generated by cycles in the VASS; this parameter refines the standard…
History-Constrained Systems
Louwe B. Kuijer, David Purser, Henry Sinclair-Banks +1
We study verification problems for history-constrained systems (HCS), a model of guarded computation that uses nested systems. An outer system describes the process architecture in…
A Note on the Parameterised Complexity of Coverability in Vector Addition Systems
Michał Pilipczuk, Sylvain Schmitz, Henry Sinclair-Banks
We investigate the parameterised complexity of the classic coverability problem for vector addition systems (VAS): given a finite set of vectors , an initi…
A Complexity Dichotomy for Semilinear Target Sets in Automata with One Counter
Yousef Shakiba, Henry Sinclair-Banks, Georg Zetzsche
In many kinds of infinite-state systems, the coverability problem has significantly lower complexity than the reachability problem. In order to delineate the border of computationa…
The Tractability Border of Reachability in Simple Vector Addition Systems with States
Dmitry Chistikov, Wojciech Czerwiński, Filip Mazowiecki +3
Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. The central algorithmic challenge in VASS is the reachability pro…
Invariants for One-Counter Automata with Disequality Tests
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks +1
We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value.…
Acyclic Petri and Workflow Nets with Resets
Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman +2
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…
Dimension-Minimality and Primality of Counter Nets
Shaull Almagor, Guy Avni, Henry Sinclair-Banks +1
A -Counter Net (-CN) is a finite-state automaton equipped with integer counters that are not allowed to become negative, but do not have explicit zero tests. This languag…
Coverability in VASS Revisited: Improving Rackoff's Bound to Obtain Conditional Optimality
Marvin Künnemann, Filip Mazowiecki, Lia Schütze +2
Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodi…
Coverability in 2-VASS with One Unary Counter is in NP
Filip Mazowiecki, Henry Sinclair-Banks, Karol Węgrzycki
Coverability in Petri nets finds applications in verification of safety properties of reactive systems. We study coverability in the equivalent model: Vector Addition Systems with…