35 citations · 102 across the 18 of their papers we have counts for
14 papers · 1 filter
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
Michael Blondin, Michaël Cadilhac, Xin-Yi Cui +3
Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checkin…
Verifying linear temporal specifications of constant-rate multi-mode systems
Michael Blondin, Philip Offtermatt, Alex Sansfaçon-Buchanan
Constant-rate multi-mode systems (MMS) are hybrid systems with finitely many modes and real-valued variables that evolve over continuous time according to mode-specific constant ra…
Separators in Continuous Petri Nets
Michael Blondin, Javier Esparza
Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking cannot reach a marking ,…
Verifying generalised and structural soundness of workflow nets via relaxations
Michael Blondin, Filip Mazowiecki, Philip Offtermatt
Workflow nets are a well-established mathematical formalism for the analysis of business processes arising from either modeling tools or process mining. The central decision proble…
The complexity of soundness in workflow nets
Michael Blondin, Filip Mazowiecki, Philip Offtermatt
Workflow nets are a popular variant of Petri nets that allow for algorithmic formal analysis of business processes. The central decision problems concerning workflow nets deal with…
Directed Reachability for Infinite-State Systems
Michael Blondin, Christoph Haase, Philip Offtermatt
Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachabilit…
Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
Michael Blondin, Javier Esparza, Martin Helfrich +2
We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a…
Affine Extensions of Integer Vector Addition Systems with States
Michael Blondin, Christoph Haase, Filip Mazowiecki +1
We study the reachability problem for affine -VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the cou…
The Complexity of Reachability in Affine Vector Addition Systems with States
Michael Blondin, Mikhail Raskin
Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches…
Automatic Analysis of Expected Termination Time for Population Protocols
Michael Blondin, Javier Esparza, Antonín Kučera
Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infini…
Forward Analysis for WSTS, Part III: Karp-Miller Trees
Michael Blondin, Alain Finkel, Jean Goubault-Larrecq
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…
Towards Efficient Verification of Population Protocols
Michael Blondin, Javier Esparza, Stefan Jaax +1
Population protocols are a well established model of computation by anonymous, identical finite state agents. A protocol is well-specified if from every initial configuration, all…
Well Behaved Transition Systems
Michael Blondin, Alain Finkel, Pierre McKenzie
The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weak…
Approaching the Coverability Problem Continuously
Michael Blondin, Alain Finkel, Christoph Haase +1
The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challe…