DROPS

Issue

Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, 2022

LITES, Volume 8, Issue 2

Editors: Alessandro Abate, Uli Fahrenberg, and Martin Fränzle

Special Issue on Distributed Hybrid Systems

Document

DOI: 10.4230/LIPIcs.CSL.2026.43

Kamp Theorem for Pomset Languages of Higher Dimensional Automata

Authors: Emily Clement, Enzo Erlich, and Jérémy Ledent

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

Temporal logics are a powerful tool to specify properties of computational systems. For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages. In the case of words, Kamp’s theorem states that First Order (FO) logic is as expressive as Linear Temporal Logic (LTL). In this paper, we extend this result to pomsets. To do so, we first investigate the class of pomset languages that are definable in FO. As expected, this is a strict subclass of MSO-definable languages. Then, we define a Linear Temporal Logic for pomsets (LTL_Poms), and show that it is equivalent to FO.

Cite as

Emily Clement, Enzo Erlich, and Jérémy Ledent. Kamp Theorem for Pomset Languages of Higher Dimensional Automata. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 43:1-43:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{clement_et_al:LIPIcs.CSL.2026.43,
  author =	{Clement, Emily and Erlich, Enzo and Ledent, J\'{e}r\'{e}my},
  title =	{{Kamp Theorem for Pomset Languages of Higher Dimensional Automata}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{43:1--43:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.43},
  URN =		{urn:nbn:de:0030-drops-254685},
  doi =		{10.4230/LIPIcs.CSL.2026.43},
  annote =	{Keywords: Higher dimensional automata, temporal logic, Kamp’s theorem}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2025.8

Parameterized Verification of Timed Networks with Clock Invariants

Authors: Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract

We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed networks (DTNs), i.e., networks of TAs that communicate via location guards that enable a transition only if there is another process in a certain location. We solve for the first time the case with unrestricted clock invariants, and establish that the parameterized model checking problem (PMCP) over finite local traces can be reduced to the corresponding model checking problem on a single TA. Moreover, we prove that the PMCP for networks that communicate via lossy broadcast can be reduced to the PMCP for DTNs. Finally, we show that for networks with k-wise synchronization, and therefore also for timed Petri nets, location reachability can be reduced to location reachability in DTNs. As a consequence we can answer positively the open problem from Abdulla et al. (2018) whether the universal safety problem for timed Petri nets with multiple clocks is decidable.

Cite as

Étienne André, Swen Jacobs, Shyam Lal Karra, and Ocan Sankur. Parameterized Verification of Timed Networks with Clock Invariants. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.FSTTCS.2025.8,
  author =	{Andr\'{e}, \'{E}tienne and Jacobs, Swen and Karra, Shyam Lal and Sankur, Ocan},
  title =	{{Parameterized Verification of Timed Networks with Clock Invariants}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.8},
  URN =		{urn:nbn:de:0030-drops-250878},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.8},
  annote =	{Keywords: Networks of Timed Automata, Parameterized Verification, Timed Petri Nets}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.29

Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems

Authors: Caroline Lemke and Benjamin Bisping

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract

We provide a generic decision procedure for energy games with energy-bounded attacker and reachability objective, moving beyond vector-valued energies and vector-addition updates. All we demand is that energies form well-founded bounded join-semilattices, and that energy updates have an upward-closed domain and can be "undone" through a Galois-connected function. We instantiate these Galois energy games to common energy games, declining energy games, multi-weighted reachability games, coverability on vector addition systems with states, and shortest path problems, supported by an Isabelle-formalization and two implementations. For the instantiations, our simple algorithm is polynomial w.r.t. game graph size and exponential w.r.t. dimension.

Cite as

Caroline Lemke and Benjamin Bisping. Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lemke_et_al:LIPIcs.CONCUR.2025.29,
  author =	{Lemke, Caroline and Bisping, Benjamin},
  title =	{{Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{29:1--29:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.29},
  URN =		{urn:nbn:de:0030-drops-239795},
  doi =		{10.4230/LIPIcs.CONCUR.2025.29},
  annote =	{Keywords: Energy games, Galois connection, Reachability, Game theory, Decidability}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2025.31

Higher-Dimensional Automata: Extension to Infinite Tracks

Authors: Luc Passemard, Amazigh Amrane, and Uli Fahrenberg

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

We introduce higher-dimensional automata for infinite interval ipomsets (ω-HDAs). We define key concepts from different points of view, inspired from their finite counterparts. Then we explore languages recognized by ω-HDAs under Büchi and Muller semantics. We show that Muller acceptance is more expressive than Büchi acceptance and, in contrast to the finite case, both semantics do not yield languages closed under subsumption. Then, we adapt the original rational operations to deal with ω-HDAs and show that while languages of ω-HDAs are ω-rational, not all ω-rational languages can be expressed by ω-HDAs.

Cite as

Luc Passemard, Amazigh Amrane, and Uli Fahrenberg. Higher-Dimensional Automata: Extension to Infinite Tracks. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{passemard_et_al:LIPIcs.FSCD.2025.31,
  author =	{Passemard, Luc and Amrane, Amazigh and Fahrenberg, Uli},
  title =	{{Higher-Dimensional Automata: Extension to Infinite Tracks}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{31:1--31:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.31},
  URN =		{urn:nbn:de:0030-drops-236466},
  doi =		{10.4230/LIPIcs.FSCD.2025.31},
  annote =	{Keywords: Higher-dimensional automata, concurrency theory, omega pomsets, B\"{u}chi acceptance, Muller acceptance, interval pomsets, pomsets with interfaces}
}

Document

DOI: 10.4230/LIPIcs.STACS.2025.8

Tropical Proof Systems: Between R(CP) and Resolution

Authors: Yaroslav Alekseev, Dima Grigoriev, and Edward A. Hirsch

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract

Propositional proof complexity deals with the lengths of polynomial-time verifiable proofs for Boolean tautologies. An abundance of proof systems is known, including algebraic and semialgebraic systems, which work with polynomial equations and inequalities, respectively. The most basic algebraic proof system is based on Hilbert’s Nullstellensatz [Paul Beame et al., 1996]. Tropical ("min-plus") arithmetic has many applications in various areas of mathematics. The operations are the real addition (as the tropical multiplication) and the minimum (as the tropical addition). Recently, [Bertram and Easton, 2017; Dima Grigoriev and Vladimir V. Podolskii, 2018; Joo and Mincheva, 2018] demonstrated a version of Nullstellensatz in the tropical setting. In this paper we introduce (semi)algebraic proof systems that use min-plus arithmetic. For the dual-variable encoding of Boolean variables (two tropical variables x and x ̅ per one Boolean variable x) and {0,1}-encoding of the truth values, we prove that a static (Nullstellensatz-based) tropical proof system polynomially simulates daglike resolution and also has short proofs for the propositional pigeon-hole principle. Its dynamic version strengthened by an additional derivation rule (a tropical analogue of resolution by linear inequality) is equivalent to the system Res(LP) (aka R(LP)), which derives nonnegative linear combinations of linear inequalities; this latter system is known to polynomially simulate Krajíček’s Res(CP) (aka R(CP)) with unary coefficients. Therefore, tropical proof systems give a finer hierarchy of proof systems below Res(LP) for which we still do not have exponential lower bounds. While the "driving force" in Res(LP) is resolution by linear inequalities, dynamic tropical systems are driven solely by the transitivity of the order, and static tropical proof systems are based on reasoning about differences between the input linear functions. For the truth values encoded by {0,∞}, dynamic tropical proofs are equivalent to Res(∞), which is a small-depth Frege system called also DNF resolution. Finally, we provide a lower bound on the size of derivations of a much simplified tropical version of the {Binary Value Principle} in a static tropical proof system. Also, we establish the non-deducibility of the tropical resolution rule in this system and discuss axioms for Boolean logic that do not use dual variables. In this extended abstract, full proofs are omitted.

Cite as

Yaroslav Alekseev, Dima Grigoriev, and Edward A. Hirsch. Tropical Proof Systems: Between R(CP) and Resolution. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{alekseev_et_al:LIPIcs.STACS.2025.8,
  author =	{Alekseev, Yaroslav and Grigoriev, Dima and Hirsch, Edward A.},
  title =	{{Tropical Proof Systems: Between R(CP) and Resolution}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.8},
  URN =		{urn:nbn:de:0030-drops-228332},
  doi =		{10.4230/LIPIcs.STACS.2025.8},
  annote =	{Keywords: Cutting Planes, Nullstellensatz refutations, Res(CP), semi-algebraic proofs, tropical proof systems, tropical semiring}
}

Document

DOI: 10.4230/LIPIcs.CSL.2025.18

Reachability for Multi-Priced Timed Automata with Positive and Negative Rates

Authors: Andrew Scoones, Mahsa Shirmohammadi, and James Worrell

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are read-once variables: they do not affect the control flow of the automaton and their value is output only at the end of a run. Thus MPTA lie between timed and hybrid automata in expressiveness. Previous work considered observers with non-negative slope in every location. In this paper we treat observers that have both positive and negative rates. Our main result is an algorithm to decide a gap version of the reachability problem for this variant of MPTA. We translate the gap reachability problem into a gap satisfiability problem for mixed integer-real systems of nonlinear constraints. Our main technical contribution - a result of independent interest - is a procedure to solve such contraints via a combination of branch-and-bound and relaxation-and-rounding.

Cite as

Andrew Scoones, Mahsa Shirmohammadi, and James Worrell. Reachability for Multi-Priced Timed Automata with Positive and Negative Rates. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 18:1-18:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{scoones_et_al:LIPIcs.CSL.2025.18,
  author =	{Scoones, Andrew and Shirmohammadi, Mahsa and Worrell, James},
  title =	{{Reachability for Multi-Priced Timed Automata with Positive and Negative Rates}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{18:1--18:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.18},
  URN =		{urn:nbn:de:0030-drops-227758},
  doi =		{10.4230/LIPIcs.CSL.2025.18},
  annote =	{Keywords: Bilinear constraints, Existential theory of real closed fields, Diophantine approximation, Pareto curve}
}

Document

DOI: 10.4230/LIPIcs.CSL.2025.33

Quantitative Graded Semantics and Spectra of Behavioural Metrics

Authors: Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/ branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems.

Cite as

Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Quantitative Graded Semantics and Spectra of Behavioural Metrics. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2025.33,
  author =	{Forster, Jonas and Schr\"{o}der, Lutz and Wild, Paul and Beohar, Harsh and Gurke, Sebastian and K\"{o}nig, Barbara and Messing, Karla},
  title =	{{Quantitative Graded Semantics and Spectra of Behavioural Metrics}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.33},
  URN =		{urn:nbn:de:0030-drops-227907},
  doi =		{10.4230/LIPIcs.CSL.2025.33},
  annote =	{Keywords: transition systems, modal logics, coalgebras, behavioural metrics}
}

Document

Introduction

DOI: 10.4230/LITES.8.2.0

Introduction to the Special Issue on Distributed Hybrid Systems

Authors: Alessandro Abate, Uli Fahrenberg, and Martin Fränzle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract

This special issue contains seven papers within the broad subject of Distributed Hybrid Systems, that is, systems combining hybrid discrete-continuous state spaces with elements of concurrency and logical or spatial distribution. It follows up on several workshops on the same theme which were held between 2017 and 2019 and organized by the editors of this volume. The first of these workshops was held in Aalborg, Denmark, in August 2017 and associated with the MFCS conference. It featured invited talks by Alessandro Abate, Martin Fränzle, Kim G. Larsen, Martin Raussen, and Rafael Wisniewski. The second workshop was held in Palaiseau, France, in July 2018, with invited talks by Luc Jaulin, Thao Dang, Lisbeth Fajstrup, Emmanuel Ledinot, and André Platzer. The third workshop was held in Amsterdam, The Netherlands, in August 2019, associated with the CONCUR conference. It featured a special theme on distributed robotics and had invited talks by Majid Zamani, Hervé de Forges, and Xavier Urbain. The vision and purpose of the DHS workshops was to connect researchers working in real-time systems, hybrid systems, control theory, formal verification, distributed computing, and concurrency theory, in order to advance the subject of distributed hybrid systems. Such systems are abundant and often safety-critical, but ensuring their correct functioning can in general be challenging. The investigation of their dynamics by analysis tools from the aforementioned domains remains fragmentary, providing the rationale behind the workshops: it was conceived that convergence and interaction of theories, methods, and tools from these different areas was needed in order to advance the subject.

Cite as

LITES, Volume 8, Issue 2: Special Issue on Distributed Hybrid Systems, pp. 0:i-0:iii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{abate_et_al:LITES.8.2.0,
  author =	{Abate, Alessandro and Fahrenberg, Uli and Fr\"{a}nzle, Martin},
  title =	{{Introduction to the Special Issue on Distributed Hybrid Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{00:1--00:3},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.0},
  URN =		{urn:nbn:de:0030-drops-192926},
  doi =		{10.4230/LITES.8.2.0},
  annote =	{Keywords: Distributed hybrid systems}
}

Document

DOI: 10.4230/LITES.8.2.3

Higher-Dimensional Timed and Hybrid Automata

Authors: Uli Fahrenberg

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract

We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata.The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.

Cite as

Uli Fahrenberg. Higher-Dimensional Timed and Hybrid Automata. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 03:1-03:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{fahrenberg:LITES.8.2.3,
  author =	{Fahrenberg, Uli},
  title =	{{Higher-Dimensional Timed and Hybrid Automata}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:16},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.3},
  URN =		{urn:nbn:de:0030-drops-192951},
  doi =		{10.4230/LITES.8.2.3},
  annote =	{Keywords: timed automaton, higher-dimensional automaton, precubical set, real time, non-interleaving concurrency, hybrid automaton}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2022.29

A Kleene Theorem for Higher-Dimensional Automata

Authors: Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemiański

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract

We prove a Kleene theorem for higher-dimensional automata (HDAs). It states that the languages they recognise are precisely the rational subsumption-closed sets of interval pomsets. The rational operations include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce HDAs with interfaces as presheaves over labelled precube categories and use tools inspired by algebraic topology, such as cylinders and (co)fibrations. HDAs are a general model of non-interleaving concurrency, which subsumes many other models in this field. Interval orders are used as models for concurrent or distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.

Cite as

Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemiański. A Kleene Theorem for Higher-Dimensional Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fahrenberg_et_al:LIPIcs.CONCUR.2022.29,
  author =	{Fahrenberg, Uli and Johansen, Christian and Struth, Georg and Ziemia\'{n}ski, Krzysztof},
  title =	{{A Kleene Theorem for Higher-Dimensional Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{29:1--29:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.29},
  URN =		{urn:nbn:de:0030-drops-170925},
  doi =		{10.4230/LIPIcs.CONCUR.2022.29},
  annote =	{Keywords: higher-dimensional automata, interval posets, Kleene theorem, concurrency theory, labelled precube categories}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2015.394

An omega-Algebra for Real-Time Energy Problems

Authors: David Cachera, Uli Fahrenberg, and Axel Legay

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract

We develop a *-continuous Kleene omega-algebra of real-time energy functions. Together with corresponding automata, these can be used to model systems which can consume and regain energy (or other types of resources) depending on available time. Using recent results on *-continuous Kleene omega-algebras and computability of certain manipulations on real-time energy functions, it follows that reachability and Büchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.

Cite as

David Cachera, Uli Fahrenberg, and Axel Legay. An omega-Algebra for Real-Time Energy Problems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 394-407, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cachera_et_al:LIPIcs.FSTTCS.2015.394,
  author =	{Cachera, David and Fahrenberg, Uli and Legay, Axel},
  title =	{{An omega-Algebra for Real-Time Energy Problems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{394--407},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.394},
  URN =		{urn:nbn:de:0030-drops-56511},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.394},
  annote =	{Keywords: Energy problem, Real time, Star-continuous Kleene algebra}
}

Document

DOI: 10.4230/LIPIcs.CALCO.2015.101

Partial Higher-dimensional Automata

Authors: Uli Fahrenberg and Axel Legay

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract

We propose a generalization of higher-dimensional automata, partial HDA. Unlike HDA, and also extending event structures and Petri nets, partial HDA can model phenomena such as priorities or the disabling of an event by another event. Using open maps and unfoldings, we introduce a natural notion of (higher-dimensional) bisimilarity for partial HDA and relate it to history-preserving bisimilarity and split bisimilarity. Higher-dimensional bisimilarity has a game characterization and is decidable in polynomial time.

Cite as

Uli Fahrenberg and Axel Legay. Partial Higher-dimensional Automata. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 101-115, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{fahrenberg_et_al:LIPIcs.CALCO.2015.101,
  author =	{Fahrenberg, Uli and Legay, Axel},
  title =	{{Partial Higher-dimensional Automata}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{101--115},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.101},
  URN =		{urn:nbn:de:0030-drops-55295},
  doi =		{10.4230/LIPIcs.CALCO.2015.101},
  annote =	{Keywords: higher-dimensional automata, bisimulation}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2011.103

The Quantitative Linear-Time--Branching-Time Spectrum

Authors: Uli Fahrenberg, Axel Legay, and Claus Thrane

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract

We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time--branching-time spectrum to a quantitative setting, parametrized by trace distance. We also provide fixed-point characterizations of all system distances, and we prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting,showing that all system distances are mutually topologically inequivalent.

Cite as

Uli Fahrenberg, Axel Legay, and Claus Thrane. The Quantitative Linear-Time--Branching-Time Spectrum. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 103-114, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{fahrenberg_et_al:LIPIcs.FSTTCS.2011.103,
  author =	{Fahrenberg, Uli and Legay, Axel and Thrane, Claus},
  title =	{{The Quantitative Linear-Time--Branching-Time Spectrum}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{103--114},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.103},
  URN =		{urn:nbn:de:0030-drops-33324},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.103},
  annote =	{Keywords: Quantitative verification, System distance, Distance hierarchy, Linear time, Branching time}
}

Document

DOI: 10.4230/DROPS.MEMICS.2009.2345

A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic

Authors: Kim G. Larsen, Uli Fahrenberg, and Claus Thrane

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)

Abstract

We extend the usual notion of Kripke Structures with a weighted transition relation, and generalize the usual Boolean satisfaction relation of CTL to a map which assigns to states and temporal formulae a real-valued distance describing the degree of satisfaction. We describe a general approach to obtaining quantitative interpretations for a generic extension of the CTL syntax, and show that, for one such interpretation, the logic is both adequate and expressive with respect to quantitative bisimulation.

Cite as

Kim G. Larsen, Uli Fahrenberg, and Claus Thrane. A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 10-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:OASIcs:2009:DROPS.MEMICS.2009.2345,
  author =	{Larsen, Kim G. and Fahrenberg, Uli and Thrane, Claus},
  title =	{{A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{10--17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2345},
  URN =		{urn:nbn:de:0030-drops-23454},
  doi =		{10.4230/DROPS.MEMICS.2009.2345},
  annote =	{Keywords: Quantitative analysis, Kripke structures, characteristic formulae, bisimulation distance, weighted CTL}
}

15 Search Results for "Fahrenberg, Uli"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message