ANR Ticktac

Nov-Dec 2020	Plenary Meeting was held online.
28-29/11/2019	Plenary Meeting was held at LRDE in Paris.
20-21/06/2019	WP3 Meeting was 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. See the list of tools we are currently developing.

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

Philipp Schlehuber-Caissier

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}
}

@inproceedings{DBLP:conf/fsttcs/BrihayeGHMQ19,
  author    = {Thomas Brihaye and
               Gilles Geeraerts and
               Marion Hallet and
               Benjamin Monmege and
               Bruno Quoitin},
  editor    = {Arkadev Chattopadhyay and
               Paul Gastin},
  title     = {Dynamics on Games: Simulation-Based Techniques and Applications to
               Routing},
  booktitle = {39th {IARCS} Annual Conference on Foundations of Software Technology
               and Theoretical Computer Science, {FSTTCS} 2019, December 11-13, 2019,
               Bombay, India},
  series    = {LIPIcs},
  volume    = {150},
  pages     = {35:1--35:14},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2019},
  url       = {https://doi.org/10.4230/LIPIcs.FSTTCS.2019.35},
  doi       = {10.4230/LIPIcs.FSTTCS.2019.35},
}

@inproceedings{JMMNS-formats2020,
author="Thierry Jéron,
Nicolas Markey,
David Mentré,
Reiya Noguchi,
Ocan Sankur",
title="Incremental methods
for checking real-time consistency",
booktitle="18th International Conference on Formal Modeling and Analysis of Timed Systems, {FORMATS 2020.}",
year="2020",
abstract="Requirements engineering is a key phase in the development
process. Ensuring that requirements are consistent is essential so that
they do not conflict and admit implementations. We consider the formal
verification of rt-consistency, which imposes that the inevitability of
definitive errors of a requirement should be anticipated, and that of
partial consistency, which was recently introduced as a more effective
check. We generalize and formalize both notions for discrete-time timed
automata, develop three incremental algorithms, and present experimental
results.",
}

@inproceedings{HJM-formats2020,
author="Léo Henry, Thierry Jéron, Nicolas Markey",
title="Active learning of timed automata with unknown resets.",
booktitle="18th International Conference on Formal Modeling and Analysis of Timed Systems, {FORMATS 2020.}",
year="2020"
}

@inproceedings{CJMM-formats2020,
author="Emily Clément, Thierry Jéron, Nicolas Markey, David Mentré",
title="Computing maximmaly-permissive strategies in acyclic timed games.",
booktitle="18th International Conference on Formal Modeling and Analysis of Timed Systems, {FORMATS 2020.}",
year="2020"
}

@article{HSTW-acm2020,
  author    = {Frédéric Herbreteau and
               B. Srivathsan and
               Thanh-Tung Tran and
               Igor Walukiewicz},
  title     = {Why Liveness for Timed Automata Is Hard, and What We Can Do About
               It},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {21},
  number    = {3},
  pages     = {17:1--17:28},
  year      = {2020},
  url       = {https://doi.org/10.1145/3372310},
  doi       = {10.1145/3372310},
}

@inproceedings{WHP-formats2020,
author="Simon Wimmer, Frédéric Herbreteau, Jaco van de Pol",
title="Certifying Emptiness of Timed Büchi Automata.",
booktitle="18th International Conference on Formal Modeling and Analysis of Timed Systems, {FORMATS 2020.}",
year="2020"
}

@article{faoc-BBFLMR,
  author =              {Bacci, Giovanni and Bouyer, Patricia and
                         Fahrenberg, Uli and Larsen, Kim Guldstrand and
                         Markey, Nicolas and Reynier, Pierre-Alain},
  title =               {Optimal and Robust Controller Synthesis Using
                         Energy Timed Automata with Uncertainty},
  journal =             {Formal Aspects of Computing},
  publisher =           {Springer},
  year =                {2020},
  note =                {To appear},
}

@inproceedings{DBLP:conf/concur/MonmegePR20,
  author    = {Benjamin Monmege and
               Julie Parreaux and
               Pierre{-}Alain Reynier},
  editor    = {Igor Konnov and
               Laura Kov{\'{a}}cs},
  title     = {Reaching Your Goal Optimally by Playing at Random with No Memory},
  booktitle = {31st International Conference on Concurrency Theory, {CONCUR} 2020,
               September 1-4, 2020, Vienna, Austria (Virtual Conference)},
  series    = {LIPIcs},
  volume    = {171},
  pages     = {26:1--26:21},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2020},
  url       = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.26},
  doi       = {10.4230/LIPIcs.CONCUR.2020.26},
}

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