Journal papers and book chapters
- 2024
- with Krzysztof Ziemiański:
Myhill-Nerode Theorem for Higher-Dimensional Automata.
Fundamenta Informaticae 192(3-4): 219-259 (2024).
- 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
- 2024
- with Roland Glück and Wesley Fussner:
Proceedings RAMiCS 2024.
Lecture Notes in Computer Science 14787, Springer, 2024.
- 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 Safa Zouari and Krzysztof Ziemiański:
Bisimulations and Logics for Higher-Dimensional Automata.
ICTAC 2024.
- with Amazigh Amrane, Hugo Bazille, Emily Clement, and Krzysztof Ziemiański:
Presenting Interval Pomsets with Interfaces.
RAMiCS 2024.
- with Amazigh Amrane, Hugo Bazille, and Marie Fortin:
Logic and Languages of Higher-Dimensional Automata.
DLT 2024.
- with Amazigh Amrane, Hugo Bazille, and Emily Clement:
Languages of Higher-Dimensional Timed Automata.
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.