Journal papers and book chapters

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.
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.
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.
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.
2014
with Axel Legay: General Quantitative Specification Theories with Modal Transition Systems. Acta Informatica 51(5):261-295.
with Axel Legay: The Quantitative Linear-Time--Branching-Time Spectrum. Theoretical Computer Science 538:54-69.
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.
with Benoît Delahaye, Kim G. Larsen and Axel Legay: Refinement and Difference for Probabilistic Automata. Logical Methods in Computer Science 10(3:11).
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.
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.
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.
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.
2011
with Kim G. Larsen and Claus Thrane: Metrics for weighted transition systems: Axiomatization and complexity. Theoretical Computer Science, 412(28):3358-3369.
with Patricia Bouyer, Kim G. Larsen, and Nicolas Markey: Quantitative analysis of real-time systems. Communications of the ACM, 54(9):78-87.
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. To be published.
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.

Books

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

2017
with Axel Legay: A Linear-Time Branching-Time Spectrum of Behavioral Specification Theories. SOFSEM 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

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

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.