Skip to main content
main-content

Über dieses Buch


This open access book constitutes the proceedings of the 22nd International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2019, which took place in Prague, Czech Republic, in April 2019, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2019.The 29 papers presented in this volume were carefully reviewed and selected from 85 submissions. They deal with foundational research with a clear significance for software science.

Unsere Produktempfehlungen

Premium-Abo der Gesellschaft für Informatik

Sie erhalten uneingeschränkten Vollzugriff auf alle acht Fachgebiete von Springer Professional und damit auf über 45.000 Fachbücher und ca. 300 Fachzeitschriften.

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Basis-Abo der Gesellschaft für Informatik

Sie erhalten uneingeschränkten Vollzugriff auf die Inhalte der Fachgebiete Business IT + Informatik und Management + Führung und damit auf über 30.000 Fachbücher und ca. 130 Fachzeitschriften.

Weitere Produktempfehlungen anzeigen

Inhaltsverzeichnis

Frontmatter

Open Access

Universal Graphs and Good for Games Automata: New Tools for Infinite Duration Games

Abstract
In this paper, we give a self contained presentation of a recent breakthrough in the theory of infinite duration games: the existence of a quasipolynomial time algorithm for solving parity games. We introduce for this purpose two new notions: good for small games automata and universal graphs.
The first object, good for small games automata, induces a generic algorithm for solving games by reduction to safety games. We show that it is in a strong sense equivalent to the second object, universal graphs, which is a combinatorial notion easier to reason with. Our equivalence result is very generic in that it holds for all existential memoryless winning conditions, not only for parity conditions.
Thomas Colcombet, Nathanaël Fijalkow

Open Access

Resource-Tracking Concurrent Games

Abstract
We present a framework for game semantics based on concurrent games, that keeps track of resources as data modified throughout execution but not affecting its control flow. Our leading example is time, yet the construction is in fact parametrized by a resource bimonoid \(\mathcal {R}\), an algebraic structure expressing resources and the effect of their consumption either sequentially or in parallel. Relying on our construction, we give a sound resource-sensitive denotation to \(\mathcal {R}\)-IPA, an affine higher-order concurrent programming language with shared state and a primitive for resource consumption in \(\mathcal {R}\). Compared with general operational semantics parametrized by \(\mathcal {R}\), our resource analysis turns out to be finer, leading to non-adequacy. Yet, our model is not degenerate as adequacy holds for an operational semantics specialized to time.
In regard to earlier semantic frameworks for tracking resources, the main novelty of our work is that it is based on a non-interleaving semantics, and as such accounts for parallel use of resources accurately.
Aurore Alcolei, Pierre Clairambault, Olivier Laurent

Open Access

Change Actions: Models of Generalised Differentiation

Abstract
Change structures, introduced by Cai et al., have recently been proposed as a semantic framework for incremental computation. We generalise change actions, an alternative to change structures, to arbitrary cartesian categories and propose the notion of change action model as a categorical model for (higher-order) generalised differentiation. Change action models naturally arise from many geometric and computational settings, such as (generalised) cartesian differential categories, group models of discrete calculus, and Kleene algebra of regular expressions. We show how to build canonical change action models on arbitrary cartesian categories, reminiscent of the Fàa di Bruno construction.
Mario Alvarez-Picallo, C.-H. Luke Ong

Open Access

Coalgebra Learning via Duality

Abstract
Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. In this paper, we generalise learning to the theory of coalgebras. The approach relies on the use of logical formulas as tests, based on a dual adjunction between states and logical theories. This allows us to learn, e.g., labelled transition systems, using Hennessy-Milner logic. Our main contribution is an abstract learning algorithm, together with a proof of correctness and termination.
Simone Barlocco, Clemens Kupke, Jurriaan Rot

Open Access

Tight Worst-Case Bounds for Polynomial Loop Programs

Abstract
In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming language—representing non-deterministic imperative programs with bounded loops, and arithmetics limited to addition and multiplication—it is possible to decide precisely whether a program has certain growth-rate properties, in particular whether a computed value, or the program’s running time, has a polynomial growth rate.
A natural and intriguing problem was to improve the precision of the information obtained. This paper shows how to obtain asymptotically-tight multivariate polynomial bounds for this class of programs. This is a complete solution: whenever a polynomial bound exists it will be found.
Amir M. Ben-Amram, Geoff W. Hamilton

Open Access

A Complete Normal-Form Bisimilarity for State

Abstract
We present a sound and complete bisimilarity for an untyped \(\lambda \)-calculus with higher-order local references. Our relation compares values by applying them to a fresh variable, like normal-form bisimilarity, and it uses environments to account for the evolving store. We achieve completeness by a careful treatment of evaluation contexts comprising open stuck terms. This work improves over Støvring and Lassen’s incomplete environment-based normal-form bisimilarity for the \(\lambda \rho \)-calculus, and confirms, in relatively elementary terms, Jaber and Tabareau’s result, that the state construct is discriminative enough to be characterized with a bisimilarity without any quantification over testing arguments.
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk

Open Access

Identifiers in Registers

Describing Network Algorithms with Logic
Abstract
We propose a formal model of distributed computing based on register automata that captures a broad class of synchronous network algorithms. The local memory of each process is represented by a finite-state controller and a fixed number of registers, each of which can store the unique identifier of some process in the network. To underline the naturalness of our model, we show that it has the same expressive power as a certain extension of first-order logic on graphs whose nodes are equipped with a total order. Said extension lets us define new functions on the set of nodes by means of a so-called partial fixpoint operator. In spirit, our result bears close resemblance to a classical theorem of descriptive complexity theory that characterizes the complexity class \(\textsc {pspace}\) in terms of partial fixpoint logic (a proper superclass of the logic we consider here).
Benedikt Bollig, Patricia Bouyer, Fabian Reiter

Open Access

The Impatient May Use Limited Optimism to Minimize Regret

Abstract
Discounted-sum games provide a formal model for the study of reinforcement learning, where the agent is enticed to get rewards early since later rewards are discounted. When the agent interacts with the environment, she may realize that, with hindsight, she could have increased her reward by playing differently: this difference in outcomes constitutes her regret value. The agent may thus elect to follow a regret- minimal strategy. In this paper, it is shown that (1) there always exist regret-minimal strategies that are admissible—a strategy being inadmissible if there is another strategy that always performs better; (2) computing the minimum possible regret or checking that a strategy is regret-minimal can be done in https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-17127-8_8/480716_1_En_8_IEq1_HTML.gif , disregarding the computational cost of numerical analysis (otherwise, this bound becomes https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-17127-8_8/480716_1_En_8_IEq2_HTML.gif ).
Michaël Cadilhac, Guillermo A. Pérez, Marie van den Bogaard

Open Access

Causality in Linear Logic

Full Completeness and Injectivity (Unit-Free Multiplicative-Additive Fragment)
Abstract
Commuting conversions of Linear Logic induce a notion of dependency between rules inside a proof derivation: a rule depends on a previous rule when they cannot be permuted using the conversions. We propose a new interpretation of proofs of Linear Logic as causal invariants which captures exactly this dependency. We represent causal invariants using game semantics based on general event structures, carving out, inside the model of [6], a submodel of causal invariants. This submodel supports an interpretation of unit-free Multiplicative Additive Linear Logic with MIX (MALL\(^-\)) which is (1) fully complete: every element of the model is the denotation of a proof and (2) injective: equality in the model characterises exactly commuting conversions of MALL\(^-\). This improves over the standard fully complete game semantics model of MALL\(^-\).
Simon Castellan, Nobuko Yoshida

Open Access

Rewriting Abstract Structures: Materialization Explained Categorically

Abstract
The paper develops an abstract (over-approximating) semantics for double-pushout rewriting of graphs and graph-like objects. The focus is on the so-called materialization of left-hand sides from abstract graphs, a central concept in previous work. The first contribution is an accessible, general explanation of how materializations arise from universal properties and categorical constructions, in particular partial map classifiers, in a topos. Second, we introduce an extension by enriching objects with annotations and give a precise characterization of strongest post-conditions, which are effectively computable under certain assumptions.
Andrea Corradini, Tobias Heindel, Barbara König, Dennis Nolte, Arend Rensink

Open Access

Two-Way Parikh Automata with a Visibly Pushdown Stack

Abstract
In this paper, we investigate the complexity of the emptiness problem for Parikh automata equipped with a pushdown stack. Pushdown Parikh automata extend pushdown automata with counters which can only be incremented and an acceptance condition given as a semi-linear set, which we represent as an existential Presburger formula over the final values of the counters. We show that the non-emptiness problem both in the deterministic and non-deterministic cases is NP-c. If the input head can move in a two-way fashion, emptiness gets undecidable, even if the pushdown stack is visibly and the automaton deterministic. We define a restriction, called the single-use restriction, to recover decidability in the presence of two-wayness, when the stack is visibly. This syntactic restriction enforces that any transition which increments at least one dimension is triggered only a bounded number of times per input position. Our main contribution is to show that non-emptiness of two-way visibly Parikh automata which are single-use is NExpTime-c. We finally give applications to decision problems for expressive transducer models from nested words to words, including the equivalence problem.
Luc Dartois, Emmanuel Filiot, Jean-Marc Talbot

Open Access

Kleene Algebra with Hypotheses

Abstract
We study the Horn theories of Kleene algebras and star continuous Kleene algebras, from the complexity point of view. While their equational theories coincide and are PSpace-complete, their Horn theories differ and are undecidable. We characterise the Horn theory of star continuous Kleene algebras in terms of downward closed languages and we show that when restricting the shape of allowed hypotheses, the problems lie in various levels of the arithmetical or analytical hierarchy. We also answer a question posed by Cohen about hypotheses of the form \(1=S\) where S is a sum of letters: we show that it is decidable.
Amina Doumane, Denis Kuperberg, Damien Pous, Pierre Pradic

Open Access

Trees in Partial Higher Dimensional Automata

Abstract
In this paper, we give a new definition of partial Higher Dimension Automata using lax functors. This definition is simpler and more natural from a categorical point of view, but also matches more clearly the intuition that pHDA are Higher Dimensional Automata with some missing faces. We then focus on trees. Originally, for example in transition systems, trees are defined as those systems that have a unique path property. To understand what kind of unique property is needed in pHDA, we start by looking at trees as colimits of paths. This definition tells us that trees are exactly the pHDA with the unique path property modulo a notion of homotopy, and without any shortcuts. This property allows us to prove two interesting characterisations of trees: trees are exactly those pHDA that are an unfolding of another pHDA; and trees are exactly the cofibrant objects, much as in the language of Quillen’s model structure. In particular, this last characterisation gives the premisses of a new understanding of concurrency theory using homotopy theory.
Jérémy Dubut

Open Access

The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains

Abstract
This paper investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications, for prenex formulæ with quantifier prefix \(\exists ^*\forall ^*\). In analogy with first-order logic, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [\(\mathsf {BSR}(\mathsf {SL}^{\!\scriptstyle {k}})\)]. In contrast to existing work in Separation Logic, in which the universe of possible locations is assumed to be infinite, both finite and infinite universes are considered. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for \(\mathsf {BSR}(\mathsf {SL}^{\!\scriptstyle {k}})\). Then we define two non-trivial subsets thereof, that are decidable for finite and infinite satisfiability respectively, by controlling the occurrences of universally quantified variables within the scope of separating implications, as well as the polarity of the occurrences of the latter. Beside the theoretical interest, our work has natural applications in program verification, for checking that constraints on the shape of a data-structure are preserved by a sequence of transformations.
Mnacho Echenim, Radu Iosif, Nicolas Peltier

Open Access

Continuous Reachability for Unordered Data Petri Nets is in PTime

Abstract
Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly complex, and its decidability status remains open. In this paper, we consider the continuous reachability problem for UDPN, which can be seen as an over-approximation of the reachability problem. Our main result is a characterization of continuous reachability for UDPN and polynomial time algorithm for solving it. This is a consequence of a combinatorial argument, which shows that if continuous reachability holds then there exists a run using only polynomially many data values.
Utkarsh Gupta, Preey Shah, S. Akshay, Piotr Hofman

Open Access

Optimal Satisfiability Checking for Arithmetic -Calculi

Abstract
The coalgebraic \(\mu \)-calculus provides a generic semantic framework for fixpoint logics with branching types beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic \(\mu \)-calculus includes an exponential time upper bound on satisfiability checking, which however requires a well-behaved set of tableau rules for the next-step modalities. Such rules are not available in all cases of interest, in particular ones involving either integer weights as in the graded \(\mu \)-calculus, or real-valued weights in combination with non-linear arithmetic. In the present work, we prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying one-step logic, roughly described as the nesting-free next-step fragment of the logic. The bound is realized by a generic global caching algorithm that supports on-the-fly satisfiability checking. Example applications include new exponential-time upper bounds for satisfiability checking in an extension of the graded \(\mu \)-calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (two-valued) probabilistic \(\mu \)-calculus with polynomial inequalities.
Daniel Hausmann, Lutz Schröder

Open Access

Constructing Inductive-Inductive Types in Cubical Type Theory

Abstract
Inductive-inductive types are a joint generalization of mutual inductive types and indexed inductive types. In extensional type theory, inductive-inductive types can be constructed from inductive types, and this construction has been conjectured to work in intensional type theory as well. In this paper, we show that the existing construction requires Uniqueness of Identity Proofs, and present a new construction (which we conjecture generalizes) of one particular inductive-inductive type in cubical type theory, which is compatible with homotopy type theory.
Jasper Hugunin

Open Access

Causal Inference by String Diagram Surgery

Abstract
Extracting causal relationships from observed correlations is a growing area in probabilistic reasoning, originating with the seminal work of Pearl and others from the early 1990s. This paper develops a new, categorically oriented view based on a clear distinction between syntax (string diagrams) and semantics (stochastic matrices), connected via interpretations as structure-preserving functors.
A key notion in the identification of causal effects is that of an intervention, whereby a variable is forcefully set to a particular value independent of any prior dependencies. We represent the effect of such an intervention as an endofunctor which performs ‘string diagram surgery’ within the syntactic category of string diagrams. This diagram surgery in turn yields a new, interventional distribution via the interpretation functor. While in general there is no way to compute interventional distributions purely from observed data, we show that this is possible in certain special cases using a calculational tool called comb disintegration.
We showcase this technique on a well-known example, predicting the causal effect of smoking on cancer in the presence of a confounding common cause. We then conclude by showing that this technique provides simple sufficient conditions for computing interventions which apply to a wide variety of situations considered in the causal inference literature.
Bart Jacobs, Aleks Kissinger, Fabio Zanasi

Open Access

Higher-Order Distributions for Differential Linear Logic

Abstract
Linear Logic was introduced as the computational counterpart of the algebraic notion of linearity. Differential Linear Logic refines Linear Logic with a proof-theoretical interpretation of the geometrical process of differentiation. In this article, we construct a polarized model of Differential Linear Logic satisfying computational constraints such as an interpretation for higher-order functions, as well as constraints inherited from physics such as a continuous interpretation for spaces. This extends what was done previously by Kerjean for first order Differential Linear Logic without promotion. Concretely, we follow the previous idea of interpreting the exponential of Differential Linear Logic as a space of higher-order distributions with compact-support, which is constructed as an inductive limit of spaces of distributions on Euclidean spaces. We prove that this exponential is endowed with a co-monadic like structure, with the notable exception that it is functorial only on isomorphisms. Interestingly, as previously argued by Ehrhard, this still allows the interpretation of differential linear logic without promotion.
Marie Kerjean, Jean-Simon Pacaud Lemay

Open Access

Languages Ordered by the Subword Order

Abstract
We consider a language together with the subword relation, the cover relation, and regular predicates. For such structures, we consider the extension of first-order logic by threshold- and modulo-counting quantifiers. Depending on the language, the used predicates, and the fragment of the logic, we determine four new combinations that yield decidable theories. These results extend earlier ones where only the language of all words without the cover relation and fragments of first-order logic were considered.
Dietrich Kuske, Georg Zetzsche

Open Access

Strong Adequacy and Untyped Full-Abstraction for Probabilistic Coherence Spaces

Abstract
We consider the probabilistic untyped lambda-calculus and prove a stronger form of the adequacy property for probabilistic coherence spaces (PCoh), showing how the denotation of a term statistically distributes over the denotations of its head-normal forms.
We use this result to state a precise correspondence between PCoh and a notion of probabilistic Nakajima trees, recently introduced by Leventis in order to prove a separation theorem. As a consequence, we get full abstraction for PCoh. This latter result has already been mentioned as a corollary of Clairambault and Paquet’s full abstraction theorem for probabilistic concurrent games. Our approach allows to prove the property directly, without the need of a third model.
Thomas Leventis, Michele Pagani

Open Access

A Sound and Complete Logic for Algebraic Effects

Abstract
This work investigates three notions of program equivalence for a higher-order functional language with recursion and general algebraic effects, in which programs are written in continuation-passing style. Our main contribution is the following: we define a logic whose formulas express program properties and show that, under certain conditions which we identify, the induced program equivalence coincides with a contextual equivalence. Moreover, we show that this logical equivalence also coincides with an applicative bisimilarity. We exemplify our general results with the nondeterminism, probabilistic choice, global store and I/O effects.
Cristina Matache, Sam Staton

Open Access

Equational Axiomatization of Algebras with Structure

Abstract
This paper proposes a new category theoretic account of equationally axiomatizable classes of algebras. Our approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. Our main contributions are a generic HSP theorem and a sound and complete equational logic, which are shown to encompass numerous flavors of equational axiomizations studied in the literature.
Stefan Milius, Henning Urbat

Open Access

Towards a Structural Proof Theory of Probabilistic -Calculi

Abstract
We present a structural proof system, based on the machinery of hypersequent calculi, for a simple probabilistic modal logic underlying very expressive probabilistic \(\mu \)-calculi. We prove the soundness and completeness of the proof system with respect to an equational axiomatisation and the fundamental cut-elimination theorem.
Christophe Lucas, Matteo Mio

Open Access

Partial and Conditional Expectations in Markov Decision Processes with Integer Weights

Abstract
The paper addresses two variants of the stochastic shortest path problem (“optimize the accumulated weight until reaching a goal state”) in Markov decision processes (MDPs) with integer weights. The first variant optimizes partial expected accumulated weights, where paths not leading to a goal state are assigned weight 0, while the second variant considers conditional expected accumulated weights, where the probability mass is redistributed to paths reaching the goal. Both variants constitute useful approaches to the analysis of systems without guarantees on the occurrence of an event of interest (reaching a goal state), but have only been studied in structures with non-negative weights. Our main results are as follows. There are polynomial-time algorithms to check the finiteness of the supremum of the partial or conditional expectations in MDPs with arbitrary integer weights. If finite, then optimal weight-based deterministic schedulers exist. In contrast to the setting of non-negative weights, optimal schedulers can need infinite memory and their value can be irrational. However, the optimal value can be approximated up to an absolute error of \(\epsilon \) in time exponential in the size of the MDP and polynomial in \(\log (1/\epsilon )\).
Jakob Piribauer, Christel Baier

Open Access

Equational Theories and Monads from Polynomial Cayley Representations

Abstract
We generalise Cayley’s theorem for monoids by providing an explicit formula for a (multi-sorted) equational theory represented by the type \(PX \rightarrow X\), where \(P\) is an arbitrary polynomial endofunctor with natural coefficients. From the computational perspective, examples of effects given by such theories include backtracking nondeterminism (obtained with the original Cayley representation \(X \rightarrow X\)), finite mutable state (obtained with \(n \rightarrow X\), for a constant n), and their different combinations (via \(n \times X \rightarrow X\) or \(X^n \rightarrow X\)). Moreover, we show that monads induced by such theories are implementable using the type formers available in programming languages based on a polymorphic \(\lambda \)-calculus, both as compositions of algebraic datatypes and as continuation-like monads. We give a set-theoretic model of the latter in terms of Barr-dinatural transformations. We also introduce CayMon, a tool that takes a polynomial as an input and generates the corresponding equational theory together with the two implementations of the induced monad in Haskell.
Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski

Open Access

A Dialectica-Like Interpretation of a Linear MSO on Infinite Words

Abstract
We devise a variant of Dialectica interpretation of intuitionistic linear logic for https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-17127-8_27/480716_1_En_27_IEq1_HTML.gif , a linear logic-based version \(\mathsf {MSO}\) over infinite words. https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-17127-8_27/480716_1_En_27_IEq3_HTML.gif was known to be correct and complete w.r.t. Church’s synthesis, thanks to an automata-based realizability model. Invoking Büchi-Landweber Theorem and building on a complete axiomatization of \(\mathsf {MSO}\) on infinite words, our interpretation provides us with a syntactic approach, without any further construction of automata on infinite words. Via Dialectica, as linear negation directly corresponds to switching players in games, we furthermore obtain a complete logic: either a closed formula or its linear negation is provable. This completely axiomatizes the theory of the realizability model of https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-17127-8_27/480716_1_En_27_IEq5_HTML.gif . Besides, this shows that in principle, one can solve Church’s synthesis for a given \(\forall \exists \)-formula by only looking for proofs of either that formula or its linear negation.
Pierre Pradic, Colin Riba

Open Access

Deciding Equivalence of Separated Non-nested Attribute Systems in Polynomial Time

Abstract
In 1982, Courcelle and Franchi-Zannettacci showed that the equivalence problem of separated non-nested attribute systems can be reduced to the equivalence problem of total deterministic separated basic macro tree transducers. They also gave a procedure for deciding equivalence of transducer in the latter class. Here, we reconsider this equivalence problem. We present a new alternative decision procedure and prove that it runs in polynomial time. We also consider extensions of this result to partial transducers and to the case where parameters of transducers accumulate strings instead of trees.
Helmut Seidl, Raphaela Palenta, Sebastian Maneth

Open Access

Justness

A Completeness Criterion for Capturing Liveness Properties (Extended Abstract)
Abstract
This paper poses that transition systems constitute a good model of distributed systems only in combination with a criterion telling which paths model complete runs of the represented systems. Among such criteria, progress is too weak to capture relevant liveness properties, and fairness is often too strong; for typical applications we advocate the intermediate criterion of justness. Previously, we proposed a definition of justness in terms of an asymmetric concurrency relation between transitions. Here we define such a concurrency relation for the transition systems associated to the process algebra CCS as well as its extensions with broadcast communication and signals, thereby making these process algebras suitable for capturing liveness properties requiring justness.
Rob van Glabbeek

Open Access

Path Category for Free

Open Morphisms from Coalgebras with Non-deterministic Branching
Abstract
There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebra for a functor G, where a bisimulation is defined as a span of G-coalgebra homomorphism. Another one is in terms of path categories and open morphisms, where a bisimulation is defined as a span of open morphisms. This similarity is no coincidence: given a functor G, fulfilling certain conditions, we derive a path-category for pointed G-coalgebras and lax homomorphisms, such that the open morphisms turn out to be precisely the G-coalgebra homomorphisms. The above construction provides path-categories and trace semantics for free for different flavours of transition systems: (1) non-deterministic tree automata (2) regular nondeterministic nominal automata (RNNA), an expressive automata notion living in nominal sets (3) multisorted transition systems. This last instance relates to Lasota’s construction, which is in the converse direction.
Thorsten Wißmann, Jérémy Dubut, Shin-ya Katsumata, Ichiro Hasuo

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise