arXiv subjects

Yann Thierry-Mieg

Publications and source records attributed to Yann Thierry-Mieg.

7 recordsLinked to original sources

arXiv2025

Structural Reductions and Stutter Sensitive Properties

Verification of properties expressed as $ω$-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a \emph{reduction} of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. We also present an approach that can reason using a partition of a property language into its stutter insensitive, shortening insensitive, lengthening insensitive and length sensitive parts to still use structural reductions even when working with arbitrary properties. An implementation and experimental evidence is provided showing most non-random properties sensitive to stutter are actually shortening or lengthening insensitive.

cs.FL↗

arXiv2025

Simplifying LTL Model Checking Given Prior Knowledge

We consider the problem of the verification of an LTL specification $φ$ on a system $S$ given some prior knowledge $K$, an LTL formula that $S$ is known to satisfy. The automata-theoretic approach to LTL model checking is implemented as an emptiness check of the product $S\otimes A_{\lnotφ}$ where $A_{\lnotφ}$ is an automaton for the negation of the property. We propose new operations that simplify an automaton $A_{\lnotφ}$ \emph{given} some knowledge automaton $A_K$, to produce an automaton $B$ that can be used instead of $A_{\lnotφ}$ for more efficient model checking. Our evaluation of these operations on a large benchmark derived from the MCC'22 competition shows that even with simple knowledge, half of the problems can be definitely answered without running an LTL model checker, and the remaining problems can be simplified significantly.

cs.FL↗

arXiv2023

LTL under reductions with weaker conditions than stutter-invariance

Verification of properties expressed as-regular languages such as LTL can benefit hugely from stutter-insensitivity, using a diverse set of reduction strategies. However properties that are not stutter-insensitive, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter-insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most nonrandom properties sensitive to stutter are actually shortening or lengthening insensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision procedure, the approach can still improve state of the art verification tools.

cs.CL↗

arXiv2021

Symbolic and Structural Model-Checking

Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows how to solve model-checking problems using a combination of techniques that stay in complexity proportional to the size of the net structure rather than to the state-space size. We combine an SMT based over-approximation to prove that some behaviors are unfeasible, an under-approximation using memory-less sampling of runs to find witness traces or counter-examples, and a set of structural reduction rules that can simplify both the system and the property. This approach was able to win by a clear margin the model-checking contest 2020 for reachability queries as well as deadlock detection, thus demonstrating the practical effectiveness and general applicability of the system of rules presented in this paper.

cs.DC↗

arXiv2018

Modeling a Cache Coherence Protocol with the Guarded Action Language

We present a formal model built for verification of the hardware Tera-Scale ARchitecture (TSAR), focusing on its Distributed Hybrid Cache Coherence Protocol (DHCCP). This protocol is by nature asynchronous, concurrent and distributed, which makes classical validation of the design (e.g. through testing) difficult. We therefore applied formal methods to prove essential properties of the protocol, such as absence of deadlocks, eventual consensus, and fairness.

cs.LO↗

arXiv2013

Model Checking Contest @ Petri Nets, Report on the 2013 edition

This document presents the results of the Model Checking Contest held at Petri Nets 2013 in Milano. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the third edition after two successful editions in 2011 and 2012. The participating tools were compared on several examinations (state space generation and evaluation of several types of formulæ -- reachability, LTL, CTL for various classes of atomic propositions) run on a set of common models (Place/Transition and Symmetric Petri nets). After a short overview of the contest, this paper provides the raw results from the contest, model per model and examination per examination. An HTML version of this report is also provided (http://mcc.lip6.fr).

cs.SE↗

arXiv2011

Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking

We present two new hybrid techniques that replace the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs of aggregates (symbolic sets of states) that can be interpreted as Büchi automata. These hybrid approaches allow on the one hand to use classical emptiness-check algorithms and build the graph on-the-fly, and on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. The Symbolic Observation Product assumes a globally stuttering property (e.g., LTL \ X) to aggregate states. The Self-Loop Aggregation Product} does not require the property to be globally stuttering (i.e., it can tackle full LTL), but dynamically detects and exploits a form of stuttering where possible. Our experiments show that these two variants, while incomparable with each other, can outperform other existing approaches.

cs.LO↗