ANR Ticktac

News

March 2022	Plenary Meeting was held online.
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.

About

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)

Members

IRISA (Rennes)

LaBRI (Bordeaux)

LIS (Marseille)

LSV (Cachan)

ISIR (Paris)

LRDE (Paris)

Damien Busatto-Gaston

Philipp Schlehuber-Caissier

Adrien Pommellet

Uli Fahrenberg

@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{DBLP:conf/lics/AkshayGJK19,
  author    = {S. Akshay and
               Paul Gastin and
               Vincent Jug{\'{e}} and
               Shankara Narayanan Krishna},
  title     = {Timed Systems through the Lens of Logic},
  booktitle = {34th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
               2019, Vancouver, BC, Canada, June 24-27, 2019},
  pages     = {1--13},
  publisher = {{IEEE}},
  year      = {2019},
  url       = {https://doi.org/10.1109/LICS.2019.8785684},
  doi       = {10.1109/LICS.2019.8785684},
  timestamp = {Tue, 30 Nov 2021 13:29:05 +0100},
  biburl    = {https://dblp.org/rec/conf/lics/AkshayGJK19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

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

@inproceedings{DBLP:conf/fsttcs/Gastin0S20,
  author    = {Paul Gastin and
               Sayan Mukherjee and
               B. Srivathsan},
  editor    = {Nitin Saxena and
               Sunil Simon},
  title     = {Reachability for Updatable Timed Automata Made Faster and More Effective},
  booktitle = {40th {IARCS} Annual Conference on Foundations of Software Technology
               and Theoretical Computer Science, {FSTTCS} 2020, December 14-18, 2020,
               {BITS} Pilani, {K} {K} Birla Goa Campus, Goa, India (Virtual Conference)},
  series    = {LIPIcs},
  volume    = {182},
  pages     = {47:1--47:17},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2020},
  url       = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.47},
  doi       = {10.4230/LIPIcs.FSTTCS.2020.47},
  timestamp = {Thu, 16 Sep 2021 18:08:17 +0200},
  biburl    = {https://dblp.org/rec/conf/fsttcs/Gastin0S20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tacas/AkshayGKR20,
  author    = {S. Akshay and
               Paul Gastin and
               Shankara Narayanan Krishna and
               Sparsa Roychowdhury},
  editor    = {Armin Biere and
               David Parker},
  title     = {Revisiting Underapproximate Reachability for Multipushdown Systems},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 26th International Conference, {TACAS} 2020, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {12078},
  pages     = {387--404},
  publisher = {Springer},
  year      = {2020},
  url       = {https://doi.org/10.1007/978-3-030-45190-5\_21},
  doi       = {10.1007/978-3-030-45190-5\_21},
  timestamp = {Tue, 30 Nov 2021 13:29:05 +0100},
  biburl    = {https://dblp.org/rec/conf/tacas/AkshayGKR20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cav/AkshayGP21,
  author    = {S. Akshay and
               Paul Gastin and
               Karthik R. Prakash},
  editor    = {Alexandra Silva and
               K. Rustan M. Leino},
  title     = {Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata},
  booktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
               2021, Virtual Event, July 20-23, 2021, Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {12759},
  pages     = {619--642},
  publisher = {Springer},
  year      = {2021},
  url       = {https://doi.org/10.1007/978-3-030-81685-8\_30},
  doi       = {10.1007/978-3-030-81685-8\_30},
  timestamp = {Tue, 30 Nov 2021 13:29:05 +0100},
  biburl    = {https://dblp.org/rec/conf/cav/AkshayGP21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{MonPar21,
	author = {Monmege, Benjamin and Parreaux, Julie and Reynier, Pierre-Alain},
	booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
	doi = {10.4230/LIPIcs.ICALP.2021.137},
	editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
	pages = {137:1--137:17},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Playing Stochastically in Weighted Timed Games to Emulate Memory},
	volume = {198},
	year = {2021}}
@inproceedings{DBLP:conf/concur/0001G0S22,
  author    = {S. Akshay and
               Paul Gastin and
               R. Govind and
               B. Srivathsan},
  editor    = {Bartek Klin and
               Slawomir Lasota and
               Anca Muscholl},
  title     = {Simulations for Event-Clock Automata},
  booktitle = {33rd International Conference on Concurrency Theory, {CONCUR} 2022,
               September 12-16, 2022, Warsaw, Poland},
  series    = {LIPIcs},
  volume    = {243},
  pages     = {13:1--13:18},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2022},
  url       = {https://doi.org/10.4230/LIPIcs.CONCUR.2022.13},
  doi       = {10.4230/LIPIcs.CONCUR.2022.13},
  timestamp = {Mon, 26 Sep 2022 17:09:13 +0200},
  biburl    = {https://dblp.org/rec/conf/concur/0001G0S22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{atva2022-NSJMM,
  author =              {Noguchi, Reiya and Sankur, Ocan and J{\'e}ron,
                         Thierry and Markey, Nicolas and Mentr{\'e}, David},
  title =               {Repairing Real-Time Requirements},
  editor =              {Bouajjani, Ahmed and Hol{\'\i}k, Luk{\'a}{\v s} and
                         Wu, Zhilin},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'22)},
  acronym =             {{ATVA}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  year =                {2022},
  month =               oct,
  doi =                 {10.1007/978-3-031-15839-1_11},
  note =                {To~appear},
  PDF = {https://hal.science/hal-03777464}
}
@article{DBLP:journals/lmcs/BrihayeGHLM22,
  author    = {Thomas Brihaye and
               Gilles Geeraerts and
               Axel Haddad and
               Engel Lefaucheux and
               Benjamin Monmege},
  title     = {One-Clock Priced Timed Games with Negative Weights},
  journal   = {Log. Methods Comput. Sci.},
  volume    = {18},
  number    = {3},
  year      = {2022},
  url       = {https://doi.org/10.46298/lmcs-18(3:17)2022},
  doi       = {10.46298/lmcs-18(3:17)2022},
  timestamp = {Tue, 24 Jan 2023 10:48:24 +0100},
  biburl    = {https://dblp.org/rec/journals/lmcs/BrihayeGHLM22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/concur/HerbreteauSW22,
  author    = {Fr{\'{e}}d{\'{e}}ric Herbreteau and
               B. Srivathsan and
               Igor Walukiewicz},
  editor    = {Bartek Klin and
               Slawomir Lasota and
               Anca Muscholl},
  title     = {Checking Timed B{\"{u}}chi Automata Emptiness Using the Local-Time
               Semantics},
  booktitle = {33rd International Conference on Concurrency Theory, {CONCUR} 2022,
               September 12-16, 2022, Warsaw, Poland},
  series    = {LIPIcs},
  volume    = {243},
  pages     = {12:1--12:24},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2022},
  url       = {https://doi.org/10.4230/LIPIcs.CONCUR.2022.12},
  doi       = {10.4230/LIPIcs.CONCUR.2022.12},
  timestamp = {Mon, 26 Sep 2022 17:09:13 +0200},
  biburl    = {https://dblp.org/rec/conf/concur/HerbreteauSW22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/0001HSW22,
  author    = {R. Govind and
               Fr{\'{e}}d{\'{e}}ric Herbreteau and
               B. Srivathsan and
               Igor Walukiewicz},
  editor    = {Christel Baier and
               Dana Fisman},
  title     = {Abstractions for the local-time semantics of timed automata: a foundation
               for partial-order methods},
  booktitle = {{LICS} '22: 37th Annual {ACM/IEEE} Symposium on Logic in Computer
               Science, Haifa, Israel, August 2 - 5, 2022},
  pages     = {24:1--24:14},
  publisher = {{ACM}},
  year      = {2022},
  url       = {https://doi.org/10.1145/3531130.3533343},
  doi       = {10.1145/3531130.3533343},
  timestamp = {Tue, 09 Aug 2022 12:40:57 +0200},
  biburl    = {https://dblp.org/rec/conf/lics/0001HSW22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/formats/BouyerGHSS22,
  author    = {Patricia Bouyer and
               Paul Gastin and
               Fr{\'{e}}d{\'{e}}ric Herbreteau and
               Ocan Sankur and
               B. Srivathsan},
  editor    = {Sergiy Bogomolov and
               David Parker},
  title     = {Zone-Based Verification of Timed Automata: Extrapolations, Simulations
               and What Next?},
  booktitle = {Formal Modeling and Analysis of Timed Systems - 20th International
               Conference, {FORMATS} 2022, Warsaw, Poland, September 13-15, 2022,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {13465},
  pages     = {16--42},
  publisher = {Springer},
  year      = {2022},
  url       = {https://doi.org/10.1007/978-3-031-15839-1\_2},
  doi       = {10.1007/978-3-031-15839-1\_2},
  timestamp = {Mon, 24 Oct 2022 20:51:03 +0200},
  biburl    = {https://dblp.org/rec/conf/formats/BouyerGHSS22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/concur/MonmegePR22,
  author    = {Benjamin Monmege and
               Julie Parreaux and
               Pierre{-}Alain Reynier},
  editor    = {Bartek Klin and
               Slawomir Lasota and
               Anca Muscholl},
  title     = {Decidability of One-Clock Weighted Timed Games with Arbitrary Weights},
  booktitle = {33rd International Conference on Concurrency Theory, {CONCUR} 2022,
               September 12-16, 2022, Warsaw, Poland},
  series    = {LIPIcs},
  volume    = {243},
  pages     = {15:1--15:22},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2022},
  url       = {https://doi.org/10.4230/LIPIcs.CONCUR.2022.15},
  doi       = {10.4230/LIPIcs.CONCUR.2022.15},
  timestamp = {Mon, 26 Sep 2022 17:09:13 +0200},
  biburl    = {https://dblp.org/rec/conf/concur/MonmegePR22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{sankur:hal-03947462,
  TITLE = {{Timed Automata Verification and Synthesis via Finite Automata Learning}},
  AUTHOR = {Ocan Sankur},
  URL = {https://hal.science/hal-03947462},
  BOOKTITLE = {{TACAS 2023 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}},
  ADDRESS = {Paris, France},
  YEAR = {2023},
  MONTH = Apr,
  PDF = {https://hal.science/hal-03947462/file/main.pdf},
  HAL_ID = {hal-03947462},
  HAL_VERSION = {v1},
}

@article{fmsd2023-HJM,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas},
  title =               {Control strategies for off-line testing of timed
                         systems},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  year =                {2023},
  doi =                 {10.1007/s10703-022-00403-w},
  note =                {To~appear},
  abstract =            {Partial observability and controllability are two
                         well-known issues in test-case synthesis for
                         reactive systems. We address the problem of partial
                         control in the synthesis of test cases from
                         timed-automata specifications. We extend a previous
                         approach to this problem from the untimed to the
                         timed setting. This extension requires a deep
                         reworking of the models, game interpretation and
                         test-synthesis algorithms. We exhibit strategies of
                         a game that try to minimize both cooperations of the
                         system and distance to the satisfaction of a test
                         purpose or to the next cooperation, and prove they
                         are winning under some fairness assumptions. This
                         entails that when turning those strategies into test
                         cases, we get properties such as soundness and
                         exhaustiveness of the test synthesis method. We
                         finally propose a symbolic algorithm to compute
                         those strategies.},
}

@article{DBLP:journals/lmcs/BusattoGastonMR23,
  author    = {Damien Busatto{-}Gaston and
               Benjamin Monmege and
               Pierre{-}Alain Reynier},
  title     = {Optimal controller synthesis for timed systems},
  journal   = {Log. Methods Comput. Sci.},
  volume    = {19},
  number    = {1},
  year      = {2023},
  url       = {https://doi.org/10.46298/lmcs-19(1:20)2023},
  doi       = {10.46298/lmcs-19(1:20)2023},
  timestamp = {Wed, 29 Mar 2023 13:54:55 +0200},
  biburl    = {https://dblp.org/rec/journals/lmcs/BusattoGastonMR23.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/formats/ClementPS23,
  author       = {Emily Clement and
                  Nicolas Perrin{-}Gilbert and
                  Philipp Schlehuber{-}Caissier},
  editor       = {Laure Petrucci and
                  Jeremy Sproston},
  title        = {Layered Controller Synthesis for Dynamic Multi-agent Systems},
  booktitle    = {Formal Modeling and Analysis of Timed Systems - 21st International
                  Conference, {FORMATS} 2023, Antwerp, Belgium, September 19-21, 2023,
                  Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14138},
  pages        = {50--68},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-42626-1_4},
  doi          = {10.1007/978-3-031-42626-1\_4},
  timestamp    = {Tue, 05 Sep 2023 20:33:25 +0200},
  biburl       = {https://dblp.org/rec/conf/formats/ClementPS23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cav/AkshayGGJS23,
  author       = {S. Akshay and
                  Paul Gastin and
                  R. Govind and
                  Aniruddha R. Joshi and
                  B. Srivathsan},
  editor       = {Constantin Enea and
                  Akash Lal},
  title        = {A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation},
  booktitle    = {Computer Aided Verification - 35th International Conference, {CAV}
                  2023, Paris, France, July 17-22, 2023, Proceedings, Part {I}},
  series       = {Lecture Notes in Computer Science},
  volume       = {13964},
  pages        = {266--288},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-37706-8_14},
  doi          = {10.1007/978-3-031-37706-8\_14},
  timestamp    = {Tue, 12 Sep 2023 07:57:21 +0200},
  biburl       = {https://dblp.org/rec/conf/cav/AkshayGGJS23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{shankar_et_al:LIPIcs.TIME.2023.6,
  author =	{Shankar, Saumya and Pinisetty, Srinivas and J\'{e}ron, Thierry},
  title =	{{Bounded-Memory Runtime Enforcement of Timed Properties}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19096},
  URN =		{urn:nbn:de:0030-drops-190962},
  doi =		{10.4230/LIPIcs.TIME.2023.6},
  annote =	{Keywords: Formal methods, Runtime enforcement, Bounded-memory, Timed automata}
}

@inproceedings{DBLP:conf/formats/Markey23,
  author       = {Nicolas Markey},
  editor       = {Laure Petrucci and
                  Jeremy Sproston},
  title        = {Computing the Price of Anarchy in Atomic Network Congestion Games
                  (Invited Talk)},
  booktitle    = {Formal Modeling and Analysis of Timed Systems - 21st International
                  Conference, {FORMATS} 2023, Antwerp, Belgium, September 19-21, 2023,
                  Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14138},
  pages        = {3--12},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-42626-1\_1},
  doi          = {10.1007/978-3-031-42626-1\_1},
  timestamp    = {Tue, 05 Sep 2023 20:33:25 +0200},
  biburl       = {https://dblp.org/rec/conf/formats/Markey23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-2305-10546,
  author       = {Nathana{\"{e}}l Fijalkow and
                  Nathalie Bertrand and
                  Patricia Bouyer{-}Decitre and
                  Romain Brenguier and
                  Arnaud Carayol and
                  John Fearnley and
                  Hugo Gimbert and
                  Florian Horn and
                  Rasmus Ibsen{-}Jensen and
                  Nicolas Markey and
                  Benjamin Monmege and
                  Petr Novotn{\'{y}} and
                  Mickael Randour and
                  Ocan Sankur and
                  Sylvain Schmitz and
                  Olivier Serre and
                  Mateusz Skomra},
  title        = {Games on Graphs},
  journal      = {CoRR},
  volume       = {abs/2305.10546},
  year         = {2023},
  url          = {https://doi.org/10.48550/arXiv.2305.10546},
  doi          = {10.48550/arXiv.2305.10546},
  eprinttype    = {arXiv},
  eprint       = {2305.10546},
  timestamp    = {Thu, 25 May 2023 15:41:47 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2305-10546.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{dziadek2023energy,
  title={Energy B{\"u}chi Problems},
  author={Dziadek, Sven and Fahrenberg, Uli and Schlehuber-Caissier, Philipp},
  booktitle={International Symposium on Formal Methods},
  pages={222--239},
  year={2023},
  organization={Springer}
}

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).

. p. .
Author PDF [bibtex]

ANR Ticktac

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

News

About

Members

Deliverables

Publications