Research
My main research topics are formal methods for specifying and designing correct computer systems. I have also applied these techniques to solve chronology problems in archaeology.
Chronolog: A tool for
computer-assisted chronological research.
Tools:
- The Babylon project
- The Expand, Enlarge and Check algorithm (for the safety properties of WSTS).
- The CSC tool for the computation of the coverability set of Petri nets
- The LavaBDD library implementing the LVBDD datastructure
- The MightyL tool that enables automata-based verification of the MITL logic.
Publications (drag your move above the title to read the abstract), see also Google Scholar and DBLP:
Journal papers
One-Clock Priced Timed Games with Negative Weights (with Thomas Brihaye, Axel Haddad, Engel Lefaucheux and Benjamin Monmege). Accepted for publication in Logical Methods in Computer Science, volume 18, issue 3, August 2022. [PDF file] [DOI].
Chronological Networks in Archaeology: a Formalised Scheme (with Eythan Levy, Frédéric Pluquet, Elie Piazetsky and Alexander Fantalkin). In Journal of Archaeological Science, volume 127, 2021. [PDF file, 1.3MB] [DOI] [Companion website].
On the Termination of Dynamics in Sequential Games (with Thomas Brihaye, Marion Hallet, and Stéphane Le Roux). Information and Computation, volume 272, article 104505, 2020. [PDF file, 578 KB] [DOI].
Synthesising Succinct Strategies in Safety Games with an Application to Real-time Scheduling (with Joël Goossens, Thi-Van-Anh Nguyen and Amélie Stainer). In Theoretical Computer Science, 735, pp 24-49, 2018. [PDF file, 1.2Mb] [DOI].
Pseudopolynomial Iterative Algorithm to Solve Total-Payoff Games and Min-Cost Reachability Games (with Thomas Brihaye, Axel Haddad and Benjamin Monmege). In Acta Informatica 54(1), 2017. [PDF file, 558KB] [DOI].
On the Verification of Concurrent, Asynchronous Programs with Waiting Queues (with Alexander Heußner and Jean-François Raskin). In ACM Transactions on Embedded Computing, 14(3), 2015. [BibTex] [DOI] [PDF file, 1 Mb].
ω-Petri nets: algorithms and complexity (with Alexander Heußner, M. Praveen and Jean-François Raskin). In Fundamenta Informaticæ 137:29-60, 2015. [BibTex] [DOI] [PDF file, 504 kB].
On regions and zones for event-clock automata (with Jean-François Raskin and Nathalie Sznajder). In Formal Methods in Systems Design, 45(3), Springer, 2014. [BibTex] [DOI] [PDF file, 424 kB].
Multiprocessor Schedulability of Arbitrary-Deadline Sporadic Tasks: Complexity and Antichain Algorithm (with Joël Goossens and Markus Lindström). Invited journal version of the RTNS 2011 paper. Real-Time Systems, The International Journal of Time-Critical Computing Systems, 49(2), pp 171-218, Springer, 2013. [BibTex] [DOI] [PDF file, 615 kB]. The original publication is available on springerlink.com
On the efficient computation of the coverability set for Petri nets (invited journal version of the ATVA07 paper) (with Jean-François Raskin and Laurent Van Begin). International Journal of Foundations of Computer Science, 21(2), World Scientific Publishing Company, 2010. [PDF file, 309 kB] [BibTex] [DOI]. Published version is (c) WSPC.
Le problème de couverture pour les réseaux de Petri: résultats classiques et développements récents (in French) (with Pierre Ganty, Jean-François Raskin and Laurent Van Begin). Techniques et Sciences Informatique, 29(2), Lavoisier, 2010. [PDF file, 289 kB] [BibTeX] [DOI].
Well-structured Languages (with Jean-François Raskin and Laurent Van Begin). Acta Informatica, 44(3-4), pp 249-288, Springer, 2007. [PDF file, full version, 388 kB] [BibTex] [DOI]. The original publication is available on springerlink.com
Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS (with Jean-François Raskin and Laurent Van Begin). Journal of Computer and System Sciences, volume 72(1), pp 180-203, Elsevier, 2005. [PDF file, full version, 326 kB] [BibTeX] [DOI]. Published version is (c) Elsevier Publishing.
On the omega-language expressive power of extended Petri nets (with Alain Finkel, Jean-François Raskin and Laurent Van Begin). Theoretical Computer Science, volume 356(3), pp 374-386, Elsevier, 2006. [PDF file, full version 190 kB] [BibTeX] [DOI]. Published version is (c) Elsevier Publishing.
Conference Proceedings and Technical reports
Exact schedulability test for sporadic mixed-criticality real-time systems using antichains and oracles (with Joël Goossens, Antonio Paolillo and Simon Picard). To appear in the proceedings of RTNS 2024, [PDF file, arXiv.org] [DOI]
ChronoLog: a tool for computer-assisted chronological modelling (with Eythan Levy and Frédéric Pluquet). Accepted for publication in the Proceedings of CAA 2021, to appear. [PDF file, 2.2MB]
Dynamics on Games: Simulation-Based Techniques and Applications to Routing (with Thomas Brihaye, Marion Hallet, Benjamin Monmege and Bruno Quoitin). In the proceedings of FSTTCS 2019, LIPIcs, vol. 150, Schloß Dagstuhl, 2019. [PDF file, arXiv.org] [DOI].
Safe and Optimal Scheduling for Hard and Soft Tasks (with Shibashis Guha and Jean-François Raskin). In the Proceedings of FSTTCS 2018, LIPIcs, vol. 122, Schloß Dagstuhl, 2018. [PDF file, DROPS] [DOI].
Efficient algorithms and tools for MITL model-checking and synthesis (short paper) (with Thomas Brihaye, Hs-Ming Ho, Arthur Milchior and Benjamin Monmege) In the proceedings of ICECCS 2018, IEEE. [PDF file, 277 KB] [DOI].
Dynamics and coalitions in sequential games (with Thomas Brihaye, Marion Hallet and Stéphane Le Roux). In the Proceedings of GandALF 2017, EPTCS 256, 2017. [PDF file, arXiv.org]. [DOI].
Models and Algorithms for Chronology (with Eythan Levy and Frédéric Pluquet).In the Proceedings of TIME 2017, LIPIcs, Schloß Dagstuhl, 2017. [PDF file, 366KB] [DOI].
Timed-automata-based verification of MITL over signals (with Thomas Brihaye, Hsi-Ming Ho and Benjamin Monmege). In the Proceedings of TIME 2017, LIPIcs, Schloß Dagstuhl, 2017. [PDF file, 724KB] [DOI].
A Backward Algorithm for the Multiprocessor Online Feasibility of Sporadic Tasks (with Joël Goossens and Van-Anh Nguyen). In the proceedings of ACSD 2017, IEEE, 2017. [PDF file, arXiv.org] [DOI].
Admissibility in Concurrent Games (with Nicolas Basset, Jean-François Raskin and Ocan Sankur). In the Proceedings of ICALP 2017, LIPIcs, vol. 80, Schloß Dagstuhl, 2017. [PDF file, arXiv.org] [DOI].
MightyL: A Compositional Translation from MITL to Timed Automata (with Thomas Brihaye, Hsi-Ming Ho and Benjamin Monmege). In the proceedings of CAV 2017, Lecture Notes in Computer Science 10426, Springer, 2017. [PDF file, HAL] [Companion website] [DOI]. The original publication is available on springerlink.com.
Real-time Synthesis is Hard! (with Thomas Brihaye, Morgane Estiévenart, Hsi-Ming Ho, Benjamin Monmege and Tali Sznajder). In the proceedings of FORMATS 2016, Lecture Notes in Computer Science 9884, Springer, 2016. [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com.
Efficient Energy Distribution in a Smart Grid using Multi-Player Games (with Thomas Brihaye, Amit Kumar Dhar, Axel Haddad and Benjamin Monmege). In the proceedings of the CASSTING'16 workshop at ETAPS, EPTCS 220, 2016. [PDF file, 135KB] [DOI].
Simple Priced Timed Games are not That Simple (with Thomas Brihaye, Axel Haddad, Engel Lefaucheux and Benjamin Monmege). In the proceedings of FSTTCS 2015, LIPIcs vol. 45, Schloß Dagstuhl. [PDF full version, arXiv.org] [DOI].
Quantitative Games under Failures (with Thomas Brihaye, Axel Haddad, Guillermo A. Pérez, Benjamin Monmege and Gabriel Renault). In the proceedings of FSTTCS 2015, LIPIcs vol. 45, Schloß Dagstuhl. [PDF full version, arXiv.org] [DOI].
To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games (with Thomas Brihaye, Axel Haddad and Benjamin Monmege). In the proceedings of CONCUR 2015. LIPIcs, vol. 42, Schloß Dagstuhl, 2015. [PDF full version, arXiv.org] [DOI].
Synthesising Succinct Strategies in Safety Games (with Joël Goossens and Amélie Stainer). In the proceedings of RP 2014. Lecture Notes in Computer Science 8762, Springer, 2014 [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com.
On MITL and alternating timed automata over infinite words (with Thomas Brihaye and Morgane Estiévenart). In the proceedings of FORMATS 2014. Lecture Notes in Computer Science 8711, Springer, 2014. [BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com.
Adding Negative Prices to Priced Timed Games (with Thomas Brihaye, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi). In the proceedings of CONCUR 2014. Lecture Notes in Computer Science 8704, Springer, 2014.[BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com.
Time-bounded Reachability for Hybrid Automata: Complexity and Fixpoints (with Thomas Brihaye, Laurent Doyen, Joël Ouaknine, Jean-François Raskin and James Worrell) In the proceedings of ATVA2013. Lecture Notes in Computer Science 8172, Springer, 2013.[BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com
On MITL and alternating timed automata (with Thomas Brihaye and Morgane Estiévenart). In the proceedings of FORMATS 2013, Lecture Notes in Computer Science 8053, Springer, 2013. [BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com
ω-Petri nets (with Alexander Heußner, M. Praveen and Jean-François Raskin). In the proceedings of Petri Nets 2013, Lecture Notes in Computer Science 7927, Springer, 2013. [BibTex] [PDF file, arXiv.org] [DOI]. The original publication is available on springerlink.com
Queue-Dispatch Asynchronous Systems (with Alexander Heußner and Jean-François Raskin). In the proceedings of ACSD 2013, IEEE. [BibTex] [PDF file, arXiv.org] [DOI].
A faster exact multiprocessor schedulability test for sporadic tasks (with Joël Goossens and Markus Lindström). In the proceedings of RTNS 2011. Best student paper award. [BibTex] [PDF file, ArXiv.org].
Event-clock automata: form theory to practice (with Jean-François Raskin an Tali Sznajder). In the proceedings of FORMATS 2011, Lecture Notes in Computer Science 6919, Springer, 2011. [BibTex] [DOI] [PDF file, ArXiv.org].The original publication is available on springerlink.com.
On reachability for hybrid automata over bounded time (with Thomas Brihaye, Laurent Doyen, Joël Ouaknine, Jean-François Raskin and James Worrell). In the proceedings of ICALP 2011 ICALP 2011, Lecture Notes in Computer Science 6756, Springer Verlag. [BibTex] [PDF file, ArXiv.org] [DOI]. The original publication is available on springerlink.com
Safraless procedures for timed specifications (with Barbara di Giampaolo, Tali Sznajder and Jean-François Raskin). In the Proceedings of FORMATS 2010 (invited paper), Lecture Notes in Computer Science 6246, Springer Verlag. [BibTex] [PDF file, 481 kB] [DOI]. The original publication is available on springerlink.com
Lattice-Valued Binary Decision Diagrams (with Gabrial Kalyon, Tristan Le Gall, Nicolas Maquet and Jean-François Raskin). In the Proceedings of ATVA 2010, Lecture Notes in Computer Science, volume 6252, Springer Verlag. [BibTex] [PDF file, 701 kB] [DOI] The original publication is available on springerlink.com.
Realizability of Real-Time Logics (with Laurent Doyen, Jean-François Raskin and Julien Reichert). In the proceedings of FORMATS 2009, Lecture Notes in Computer Science, volume 5813, pages 133-148, Springer Verlag. [BibTex] [PDF file, 204 kB] [DOI]. The original publication is available on springerlink.com
On the expressive power of Petri nets with transfer arcs vs. Petri nets with reset arcs. Technical report 572, ULB. [BibTex] [PDF file, 147 kB].
On the efficient Computation of the Minimal Coverability set of Petri nets (with Jean-François Raskin and Laurent Van Begin). In the Proceedings of ATVA07, Lecture Notes in Computer Science, volume 4762, pages 98-113, Springer Verlag. [BibTex] [PDF file, 238 kB] [DOI]. The original publication is available on springerlink.com
Expand, Enlarge and Check... Made Efficient (with Jean-François Raskin and Laurent Van Begin), in the Proceedings of. CAV'05, Lecture Notes in Computer Science, volume 3576, pages 394-407 Springer Verlag. [BibTex] [PDF file, 244 kB] [DOI]. The original publication is available on springerlink.com
A counter-example to the minimal coverability tree algorithm (with Alain Finkel, Jean-François Raskin and Laurent Van Begin), Technical report 535, ULB. [BibTex] [PDF file, 90 kB].
Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS (with Jean-François Raskin and Laurent Van Begin). In the Proceedings of FSTTCS 2004, Lecture Notes in Computer Science, volume 3328, pages 287--298. Springer-Verlag, 2004. [BibTeX]. Full paper (with all the proofs): [PDF file, 337 kB] [DOI]. The original publication is available on springerlink.com
On the omega-language expressive power of extended Petri nets (with Alain Finkel, Jean-François Raskin and Laurent Van Begin). In the Proceedings of EXPRESS'04, Electronic Notes in Computer Sciences, 128(2), pp 87-101, Elsevier, 2005. Pre-print version [PDF file, 305 kB] [DOI]. The proceedings version (c) Elsevier is available on Science Direct. The proofs are available in the journal version of the paper (see above). [BibTeX]. Also Technical Report 519, ULB, 2004.
Concurrent Boolean Programs (with Laurent Van Begin), Technical Report 505, ULB, 2003. [Postscript file, 583 kB] [BibTeX]
Babylon: An integrated toolkit for the specification and verification of parameterized systems (with Pierluigi Ammirati, Giorgio Delzanno, Pierre Ganty, Jean-François Raskin and Laurent Van Begin). In the Proceedings of SAVE, 2002 [PostScript file, 184 kB] [BibTeX entry].
Dissertations
Coverability and Expressiveness Properties of Well-structured Transitions Systems, PhD thesis, ULB, 2007. [PDF file, 2.1 Mb]. Slides for the FRS/FNRS IBM award: [PDF file, 3,8 Mb]
How to grind Java software to extract full-bodied infinite-state models ?, Diplome d'études approfondies, ULB, 2003. [PDF file 1.4 Mb] [Bibtex Entry] [Slides of the presentation, PDF, 1.4 Mb].
A comparison of various backward analyzers for parametrized concurrent systems, Master's thesis, ULB, 2002. [PS.GZ file, 417 kB] [Slides of the presentation, PDF] [Bibtex Entry].
Photo: V. Kuchta