ANR Ticktac

20-21/06/2019	WP3 Meeting is held at LaBRI, Bordeaux.
04-05/04/2019	Kickoff meeting was held in Rennes on April 4-5. See the programme and the slides of the talks
01/03/2019	ANR Ticktac begins!

TChecker is an open-source model checker for timed automata. Try the current version.

Keywords:	Timed automata, model checking, synthesis, timed games
Abstract:
Members:	IRISA (Rennes), LaBRI (Bordeaux), LIS (Marseille), LSV (Cachan), ISIR (Paris), LRDE (Paris)
Coordinator:	Ocan Sankur (IRISA)

IRISA (Rennes)

LaBRI (Bordeaux)

LIS (Marseille)

LSV (Cachan)

ISIR (Paris)

LRDE (Paris)

Damien Busatto-Gaston

Patricia Bouyer

Paul Gastin

Nicolas Perrin

Philipp Schlehuber-Caissier

Alexandre Duret-Lutz

Adrien Pommellet

@inproceedings{GHSW-concur19,
author={R. Govind and F. Herbreteau and B Srivathsan and I. Walukiewicz},
title={Revisiting local time semantics for networks of timed automata},
booktitle="({CONCUR}'19)",
pdf="https://arxiv.org/abs/1907.02296",
year="2019",
}

@inproceedings{BMRS-cav19,
author="Busatto-Gaston, Damien
and Monmege, Benjamin
and Reynier, Pierre-Alain
and Sankur, Ocan",
editor="Dillig, Isil
and Tasiran, Serdar",
title="Robust Controller Synthesis in Timed B{\"u}chi Automata: A Symbolic Approach",
booktitle="Computer Aided Verification  ({CAV}'19)",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="572--590",
abstract="We solve in a purely symbolic way the robust controller synthesis problem in timed automata with B{\"u}chi acceptance conditions. The goal of the controller is to play according to an accepting lasso of the automaton, while resisting to timing perturbations chosen by a competing environment. The problem was previously shown to be PSPACE-complete using regions-based techniques, but we provide a first tool solving the problem using zones only, thus more resilient to state-space explosion problem. The key ingredient is the introduction of branching constraint graphs allowing to decide in polynomial time whether a given lasso is robust, and even compute the largest admissible perturbation if it is. We also make an original use of constraint graphs in this context in order to test the inclusion of timed reachability relations, crucial for the termination criterion of our algorithm. Our techniques are illustrated using a case study on the regulation of a train network.",
isbn="978-3-030-25540-4",
url="https://link.springer.com/chapter/10.1007%2F978-3-030-25540-4_33",
pdf="https://hal.archives-ouvertes.fr/hal-02264083"
}

@inproceedings{RSM-cav19,
author="Roussanaly, Victor
and Sankur, Ocan
and Markey, Nicolas",
editor="Dillig, Isil
and Tasiran, Serdar",
title="Abstraction Refinement Algorithms for Timed Automata",
booktitle="Computer Aided Verification ({CAV}'19)",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="22--40",
abstract="We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We implement this idea in two ways: an enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.",
isbn="978-3-030-25540-4",
PDF={https://arxiv.org/abs/1905.07365},
url={https://link.springer.com/chapter/10.1007%2F978-3-030-25540-4_2}
}

@inproceedings{GMS-cav19,
author="Gastin, Paul
and Mukherjee, Sayan
and Srivathsan, B.",
editor="Dillig, Isil
and Tasiran, Serdar",
title="Fast Algorithms for Handling Diagonal Constraints in Timed Automata",
booktitle="Computer Aided Verification  ({CAV}'19)",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="41--59",
abstract="A popular method for solving reachability in timed automata proceeds by enumerating reachable sets of valuations represented as zones. A na{\"i}ve enumeration of zones does not terminate. Various termination mechanisms have been studied over the years. Coming up with efficient termination mechanisms has been remarkably more challenging when the automaton has diagonal constraints in guards.",
isbn="978-3-030-25540-4",
pdf={https://arxiv.org/abs/1904.08590},
url={https://link.springer.com/chapter/10.1007%2F978-3-030-25540-4_3}
}

}

Please add the following acknowledgement to all publications related to this project:

This work was partially funded by ANR project Ticktac (ANR-18-CE40-0015).

ANR Ticktac

Efficient Techniques and Tools for the Verification and Synthesis of Real-Time Systems

News

About

Members

Deliverables

Publications