35 citations · 81 across the 10 of their papers we have counts for
14 papers
A Zone-Based Algorithm for Timed Parity Games
Gilles Geeraerts, Frédéric Herbreteau, Jean-François Raskin +1
This paper revisits timed games by building upon the semantics introduced in "The Element of Surprise in Timed Games". We introduce some modifications to this semantics for two pri…
Revisiting Stateful Partial-Order Reduction
Frédéric Herbreteau, Sarah Larroze-Jardiné, Gérald Point +1
The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach build…
Cross--layer Formal Verification of Robotic Systems
Sylvain Raïs, Julien Brunel, David Doose +1
Robotic systems are widely used to interact with humans or to perform critical tasks. As a result, it is imperative to provide guarantees about their behavior. Due to the modularit…
Zone-based verification of timed automata: extrapolations, simulations and what next?
Patricia Bouyer, Paul Gastin, Frédéric Herbreteau +2
Timed automata have been introduced by Rajeev Alur and David Dill in the early 90's. In the last decades, timed automata have become the de facto model for the verification of real…
Certifying Emptiness of Timed Büchi Automata
Simon Wimmer, Frédéric Herbreteau, Jaco van de Pol
Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at furt…
Revisiting local time semantics for networks of timed automata
R. Govind, Frédéric Herbreteau, B. Srivathsan +1
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…
Improving search order for reachability testing in timed automata
Frédéric Herbreteau, Thanh-Tung Tran
Standard algorithms for reachability analysis of timed automata are sensitive to the order in which the transitions of the automata are taken. To tackle this problem, we propose a…
Fast detection of cycles in timed automata
Aakash Deshpande, Frédéric Herbreteau, B. Srivathsan +2
We propose a new efficient algorithm for detecting if a cycle in a timed automaton can be iterated infinitely often. Existing methods for this problem have a complexity which is ex…
Lazy abstractions for timed automata
Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz
We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. For efficiency…
Reachability of Communicating Timed Processes
Lorenzo Clemente, Frédéric Herbreteau, Amélie Stainer +1
We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises automata with local timing constraints communicating over…
Using non-convex approximations for efficient analysis of timed automata
Frédéric Herbreteau, Dileep Kini, B. Srivathsan +1
The reachability problem for timed automata asks if there exists a path from an initial state to a target state. The standard solution to this problem involves computing the zone g…
Better abstractions for timed automata
Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz
We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstracti…
Coarse abstractions make Zeno behaviours difficult to detect
Frédéric Herbreteau, B Srivathsan
An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find…
Efficient Emptiness Check for Timed Büchi Automata (Extended version)
Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz
The Büchi non-emptiness problem for timed automata refers to deciding if a given automaton has an infinite non-Zeno run satisfying the Büchi accepting condition. The standard solut…