Journal papers and book chapters

2023
with Christian Johansen, Georg Struth and Krzysztof Ziemiański: Catoids and Modal Convolution Algebras. Algebra Universalis 84(10) (2023).
2022
Higher-Dimensional Timed and Hybrid Automata. Leibniz Transactions on Embedded Systems 8(2):03:1-03:16 (2022).
with Axel Legay: Featured Games. Science of Computer Programming 223:102874 (2022).
with Christian Johansen, Georg Struth and Krzysztof Ziemiański: Posets With Interfaces as a Model for Concurrency. Information and Computation 285(B):104914 (2022).
with Christian Johansen, Georg Struth and Krzysztof Ziemiański: Domain Semirings United. Acta Cybernetica 25(3): 575-583 (2022).
2021
with Giovanni Bacci, Patricia Bouyer, Kim G. Larsen, Nicolas Markey and Pierre-Alain Reynier: Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty. Formal Aspects of Computing 33(1): 3-25 (2021).
with Christian Johansen, Christopher A. Trotter and Krzysztof Ziemiański: Sculptures in Concurrency. Logical Methods in Computer Science 17(2) (2021).
with Christian Johansen, Georg Struth and Krzysztof Ziemiański: Languages of Higher-Dimensional Automata. Mathematical Structures in Computer Science 31(5): 575-613 (2021).
2020
with Axel Legay and Karin Quaas: Computing Branching Distances Using Quantitative Games. Theoretical Computer Science 847:134-146 (2020).
with Axel Legay: A Linear-Time Branching-Time Spectrum for Behavioral Specification Theories. Journal of Logical and Algebraic Methods in Programming 110:100499 (2020).
with Nikola Beneš, Jan Křetínský, Axel Legay, and Louis-Marie Traonouez: Logical vs. behavioural specifications. Information and Computation 271:104487 (2020).
2019
with David Cachera and Axel Legay: An ω-Algebra for Real-Time Energy Problems. Logical Methods in Computer Science 15(2:17) (2019).
with Axel Legay: Quantitative properties of featured automata. Software Tools for Technology Transfer 21(6):667-677 (2019).
2018
with Jan Křetínský, Axel Legay and Louis-Marie Traonouez: Compositionality for quantitative specifications. Soft Computing 22(4): 1139-1158 (2018).
with Patricia Bouyer, Kim G. Larsen, Nicolas Markey, Joël Ouaknine, and James Worrell: Model Checking Real-Time Systems. In Handbook of Model Checking, Springer, 2018.
2017
with Zoltán Ésik, Axel Legay and Karin Quaas: An Algebraic Approach to Energy Problems I -- *-Continuous Kleene ω-Algebras. Acta Cybernetica 23(1):203-228 (2017).
with Zoltán Ésik, Axel Legay and Karin Quaas: An Algebraic Approach to Energy Problems II -- The Algebra of Energy Functions. Acta Cybernetica 23(1):229-268 (2017).
with Kim G. Larsen and Axel Legay: From timed automata to stochastic hybrid games. In Dependable Software Systems Engineering, IOS Press, 2016.
2016
with Thi Thieu Hoa Le, Roberto Passerone and Axel Legay: Contract-Based Requirement Modularization via Synthesis of Correct Decompositions. ACM Transactions on Embedded Computing Systems 15(2):33:1-26 (2016).
with Thi Thieu Hoa Le, Roberto Passerone and Axel Legay: A Tag Contract Framework for Modeling Heterogeneous Systems. Science of Computer Programming 115-116:225-246 (2016).
2014
with Axel Legay: General Quantitative Specification Theories with Modal Transition Systems. Acta Informatica 51(5):261-295 (2014).
with Axel Legay: The Quantitative Linear-Time--Branching-Time Spectrum. Theoretical Computer Science 538:54-69 (2014).
with Xavier Allamigeon, Stéphane Gaubert, Ricardo Katz and Axel Legay: Tropical Fourier-Motzkin Elimination, with an Application to Real-Time Verification. International Journal of Algebra and Computation 24(5):569-607 (2014).
with Benoît Delahaye, Kim G. Larsen and Axel Legay: Refinement and Difference for Probabilistic Automata. Logical Methods in Computer Science 10(3:11) (2014).
2013
with Sebastian S. Bauer, Line Juhl, Kim G. Larsen, Axel Legay, and Claus Thrane: Weighted Modal Transition Systems. Formal Methods in System Design, 42(2):193-220 (2013).
with Kim G. Larsen and Axel Legay: Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems. In Unifying Theories of Programming and Formal Engineering Methods, Springer, 2013.
with Kim G. Larsen and Axel Legay: Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems. In Engineering Dependable Software Systems, IOS Press, 2013.
2012
with Qi Lu, Michael Madsen, Martin Milata, Søren Ravn, and Kim G. Larsen: Reachability Analysis for Timed Automata using Max-Plus Algebra. Journal of Logic and Algebraic Programming, 81(3):298-313 (2012).
2011
with Kim G. Larsen and Claus Thrane: Metrics for weighted transition systems: Axiomatization and complexity. Theoretical Computer Science, 412(28):3358-3369 (2011).
with Patricia Bouyer, Kim G. Larsen, and Nicolas Markey: Quantitative analysis of real-time systems. Communications of the ACM, 54(9):78-87 (2011).
with Kim G. Larsen and Claus Thrane: Model-based verification and analysis for real-time systems. In Manfred Broy, David Harel, and Tony Hoare, editors, Software and Systems Safety: Specification and Verification, NATO Science for Peace and Security Series ­ D: Information and Communication Security. IOS Press, 2011.
2010
with Kim G. Larsen and Claus Thrane: A quantitative characterization of weighted Kripke structures in temporal logic. Computing and Informatics 29 (2010).
with Claus Thrane and Kim G. Larsen: Quantitative analysis of weighted transition systems. Journal of Logic and Algebraic Programming 79(7) (2010).
2009
with Kim G. Larsen and Claus Thrane: Verification, performance analysis and controller synthesis for real-time systems. In Manfred Broy, Wassiou Sitou, and Tony Hoare, editors, Engineering Methods and Tools for Software Safety and Security, volume 22 of NATO Science for Peace and Security Series ­ D: Information and Communication Security. IOS Press, 2009.
2007
with Martin Raussen: Reparametrizations of continuous paths. Journal of Homotopy and Related Structures 2(2) (2007). See also under Preprints.

Books and journal special issues

2022
with Alessandro Abate and Martin Fränzle: Special Issue on Distributed Hybrid Systems, Leibniz Transactions on Embedded Systems, 2022.
2021
with Mai Gehrke, Luigi Santocanale and Michael Winter: Proceedings RAMiCS 2021. Lecture Notes in Computer Science 13027, Springer, 2021.
2020
with Peter Jipsen and Michael Winter: Proceedings RAMiCS 2020. Lecture Notes in Computer Science 12062, Springer, 2020.
2012
with Axel Legay and Claus Thrane: Proceedings QFM 2012. EPTCS 103.
2011
with Stavros Tripakis: Proceedings FORMATS 2011. LNCS 6919, Springer.
2004
with Eric Goubault, Thomas T. Hildebrandt, and Alexander Kurz: Proceedings GETCO&CMCIM 2003. ENTCS 100, Elsevier.

Conference and workshop contributions

2024
with Amazigh Amrane, Hugo Bazille, and Marie Fortin: Logic and Languages of Higher-Dimensional Automata. Accepted for DLT 2024.
with Amazigh Amrane, Hugo Bazille, and Emily Clement: Languages of Higher-Dimensional Timed Automata. Accepted for PETRI NETS 2024.
2023
with Amazigh Amrane, Hugo Bazille, and Krzysztof Ziemiański: Closure and decision properties for higher-dimensional automata. ICTAC 2023.
with Krzysztof Ziemiański: A Myhill-Nerode theorem for higher-dimensional automata. PETRI NETS 2023. Outstanding Paper Award.
with Sven Dziadek and Philipp Schlehuber-Caissier: Energy Büchi Problems. FM 2023.
2022
with Christian Johansen, Georg Struth and Krzysztof Ziemiański: A Kleene theorem for higher-dimensional automata. CONCUR 2022.
Languages of Higher-Dimensional Automata. Highlights 2022.
2021
with Axel Legay: Featured Games. TASE 2021.
with Cameron Calk, Christian Johansen, Georg Struth and Krzysztof Ziemiański: lr-Multisemigroups, Modal Quantales and the Origin of Locality. RAMiCS 2021.
2020
with Christian Johansen, Georg Struth, and Ratan Bahadur Thapa: Generating Posets Beyond N. RAMiCS 2020.
with Axel Legay: Behavioral Specification Theories: an Algebraic Taxonomy. ISoLA 2021.
2019
with Axel Legay and Karin Quaas: Computing Branching Distances Using Quantitative Games. ICTAC 2019.
2018
Higher-Dimensional Timed Automata. ADHS 2018.
with Giovanni Bacci, Patricia Bouyer, Kim G. Larsen, Nicolas Markey and Pierre-Alain Reynier: Optimal and robust controller synthesis. FM 2018. Best Paper Award.
with Kim G. Larsen: Energiautomater, energifunktioner og Kleene-algebra. NIK 2018.
with Rafael Olaechea, Joanne M. Atlee, and Axel Legay: Trace checking for dynamic software product lines. SEAMS@ICSE 2018.
2017
with Axel Legay: A Linear-Time Branching-Time Spectrum of Behavioral Specification Theories. SOFSEM 2017.
with Meriem Ouederni, Axel Legay and Gwen Salaün: Compatibility Flooding: Measuring Interaction of Behavioural Models. ACM SAC 2017.
with Axel Legay: Featured Weighted Automata. FormaliSE@ICSE 2017.
2016
with Rafael Olaechea and Axel Legay: Long-Term Average Cost in Featured Transition Systems. SPLC 2016.
2015
with Axel Legay: Partial Higher-Dimensional Automata. CALCO 2015.
with Zoltán Ésik and Axel Legay: *-Continuous Kleene ω-Algebras. DLT 2015.
with Zoltán Ésik and Axel Legay: *-Continuous Kleene ω-Algebras for Energy Problems. FICS 2015.
with Jo Atlee and Axel Legay: Measuring Behaviour Interactions between Product-Line Features. FormaliSE@ICSE 2015.
with David Cachera and Axel Legay: An ω-Algebra for Real-Time Energy Problems. FSTTCS 2015.
with Jo Atlee, Sandy Beidu and Axel Legay: Merging Features in Featured Transition Systems. MoDeVVa@MoDELS 2015.
2014
with Jan Křetínský, Axel Legay and Louis-Marie Traonouez: Compositionality for Quantitative Specifications. FACS 2014.
with Fabrizio Biondi, Kevin Corre, Cyrille Jégourel, Simon Kongshøj and Axel Legay: Measuring Global Similarity between Texts. SLSP 2014.
with Axel Legay: Configurable Formal Methods for Extreme Modeling. XM@MoDELS 2014.
with Axel Legay and Louis-Marie Traonouez: Structural Refinement for the Modal nu-Calculus. ICTAC 2014.
with Kim G. Larsen, Axel Legay, and Louis-Marie Traonouez: Parametric and Quantitative Extensions of Modal Transition Systems. FPS@ETAPS 2014.
with Axel Legay and Louis-Marie Traonouez: Specification Theories for Probabilistic and Real-Time Systems. FPS@ETAPS 2014.
with Mathieu Acher, Axel Legay, and Andrzej Wąsowski: Sound Merging and Differencing for Class Diagrams. FASE 2014.
2013
with Zoltán Ésik, Axel Legay, and Karin Quaas: Kleene Algebras and Semimodules for Energy Problems. ATVA 2013.
with Nikola Beneš, Benoît Delahaye, Jan Křetínský, and Axel Legay: Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. CONCUR 2013.
with Axel Legay: History-Preserving Bisimilarity for Higher-Dimensional Automata via Open Maps. MFPS XXIX.
with Axel Legay: Generalized Quantitative Analysis of Metric Transition Systems. APLAS 2013.
with Thi Thieu Hoa Le, Roberto Passerone, and Axel Legay: Tag Machines for Modeling Heterogeneous Systems. ACSD 2013.
with Thi Thieu Hoa Le, Roberto Passerone, and Axel Legay: A Tag Contract Framework for Heterogeneous Systems. FOCLASA 2013.
with Benoît Delahaye, Kim G. Larsen, and Axel Legay: Refinement and Difference for Probabilistic Automata. QEST 2013.
2012
with Axel Legay: A Robust Specification Theory for Modal Event-Clock Automata. FIT 2012.
with Sebastian S. Bauer, Axel Legay, and Claus Thrane: General Quantitative Specification Theories with Modalities. CSR 2012.
with Benoît Delahaye, Thomas A. Henzinger, Axel Legay, and Dejan Ničković: Synchronous Interface Theories and Time Triggered Scheduling. FMOODS/FORTE 2012.
2011
with Axel Legay and Claus Thrane: The Quantitative Linear-Time--­Branching-Time Spectrum. FSTTCS 2011.
with Axel Legay and Andrzej Wąsowski: Make a Difference! (Semantically). MODELS 2011.
with Sebastian S. Bauer, Line Juhl, Kim G. Larsen, Axel Legay, and Claus Thrane: Quantitative Refinement for Weighted Modal Transition Systems. MFCS 2011.
with Line Juhl, Kim G. Larsen, and Jiří Srba: Energy Games in Multiweighted Automata. ICTAC 2011.
with Kim G. Larsen and Claus Thrane: Distances for Weighted Transition Systems: Games and Properties. QAPL 2011.
2010
with Jesper Dyhrberg, Qi Lu, Michael Madsen, and Søren Ravn: Computations on Zones using Max-Plus Algebra. NWPT 2010.
with Patricia Bouyer, Kim G. Larsen and Nicolas Markey: Timed automata with observers under energy constraints. HSCC 2010.
2009
with Kim G. Larsen and Claus Thrane: Verification, performance analysis and controller synthesis for real-time systems. FSEN 2009. Invited paper.
with Kim G. Larsen and Claus Thrane: A quantitative characterization of weighted Kripke structures in temporal logic. MEMICS 2009. Best paper award.
with Kim G. Larsen and Claus Thrane: A quantitative characterization of weighted Kripke structures in temporal logic. QUANTLOG 2009.
with Kim G. Larsen: Discounting in time. QAPL 2009. [Slides]
2008
with Claus Thrane and Kim G. Larsen: Quantitative simulations of weighted transition systems. NWPT 2008.
with Patricia Bouyer, Kim G. Larsen, Nicolas Markey, and Jiří Srba: Infinite runs in weighted timed automata with energy constraints. FORMATS 2008.
with Kim G. Larsen: Discount-optimal infinite runs in priced timed automata. INFINITY 2008. [Slides]
How to pull back open maps along semantics functors. ACCAT 2008. [Slides]
2005
A category of higher-dimensional automata. FOSSACS 2005. See also under Preprints.
2004
A dihomotopy double category of a po-space. GETCO 2004.
2003
Directed homology. GETCO&CMCIM 2003.
2002
The geometry of timed PV programs. GETCO 2002.
2001
Simulation of timed game automata. NWPT 2001.

Preprints

2006
with Martin Raussen: Reparametrizations of continuous paths. Research report R-2006-22, Dept. of Mathematical Sciences, Aalborg University.
2005
Bisimulation for higher-dimensional automata. A geometric interpretation. Research report R-2005-01, Dept. of Mathematical Sciences, Aalborg University.

Theses

2022
Habilitation thesis: A generic approach to quantitative verification. Université Paris-Saclay.
2005
Ph.D. thesis: Higher-dimensional automata from a topological viewpoint. Department of Mathematical Sciences, Aalborg University.
2002
Master's thesis: Towards an efficient algorithm for detecting unsafe states in timed concurrent systems. Department of Mathematical Sciences, Aalborg University.

Miscellaneous

2023
with Aline Fahrenberg: Une approche générique à la vérification quantitative. French translation of the first chapter of my habilitation thesis.
2005
Lars Gårding: Matematikken, livet og døden. Translated from Swedish into Danish, with Monica Johannsen. Matilde 24, Danish Mathematical Society.
2002
Fordelinger. A note on probability distributions, in Danish.