Search Results

Documents authored by Wißmann, Thorsten

Document
DOI: 10.4230/LIPIcs.CALCO.2023.12
Bisimilar States in Uncertain Structures

Authors: Jurriaan Rot and Thorsten Wißmann

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

Abstract
We provide a categorical notion called uncertain bisimilarity, which allows to reason about bisimilarity in combination with a lack of knowledge about the involved systems. Such uncertainty arises naturally in automata learning algorithms, where one investigates whether two observed behaviours come from the same internal state of a black-box system that can not be transparently inspected. We model this uncertainty as a set functor equipped with a partial order which describes possible future developments of the learning game. On such a functor, we provide a lifting-based definition of uncertain bisimilarity and verify basic properties. Beside its applications to Mealy machines, a natural model for automata learning, our framework also instantiates to an existing compatibility relation on suspension automata, which are used in model-based testing. We show that uncertain bisimilarity is a necessary but not sufficient condition for two states being implementable by the same state in the black-box system. We remedy the lack of sufficiency by a characterization of uncertain bisimilarity in terms of coalgebraic simulations.
Cite as

Jurriaan Rot and Thorsten Wißmann. Bisimilar States in Uncertain Structures. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{rot_et_al:LIPIcs.CALCO.2023.12,
  author =	{Rot, Jurriaan and Wi{\ss}mann, Thorsten},
  title =	{{Bisimilar States in Uncertain Structures}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.12},
  URN =		{urn:nbn:de:0030-drops-188094},
  doi =		{10.4230/LIPIcs.CALCO.2023.12},
  annote =	{Keywords: Coalgebra, Relation Lifting, Bisimilarity, Mealy Machines, ioco}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.137
Action Codes

Authors: Frits Vaandrager and Thorsten Wißmann

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We provide a new perspective on the problem how high-level state machine models with abstract actions can be related to low-level models in which these actions are refined by sequences of concrete actions. We describe the connection between high-level and low-level actions using action codes, a variation of the prefix codes known from coding theory. For each action code ℛ, we introduce a contraction operator α_ℛ that turns a low-level model ℳ into a high-level model, and a refinement operator ϱ_ℛ that transforms a high-level model 𝒩 into a low-level model. We establish a Galois connection ϱ_ℛ(𝒩) ⊑ ℳ ⇔ 𝒩 ⊑ α_ℛ(ℳ), where ⊑ is the well-known simulation preorder. For conformance, we typically want to obtain an overapproximation of model ℳ. To this end, we also introduce a concretization operator γ_ℛ, which behaves like the refinement operator but adds arbitrary behavior at intermediate points, giving us a second Galois connection α_ℛ(ℳ) ⊑ 𝒩 ⇔ ℳ ⊑ γ_ℛ(𝒩). Action codes may be used to construct adaptors that translate between concrete and abstract actions during learning and testing of Mealy machines. If Mealy machine ℳ models a black-box system then α_ℛ(ℳ) describes the behavior that can be observed by a learner/tester that interacts with this system via an adaptor derived from code ℛ. Whenever α_ℛ(ℳ) implements (or conforms to) 𝒩, we may conclude that ℳ implements (or conforms to) γ_ℛ (𝒩). Almost all results, examples, and counter-examples are formalized in Coq.
Cite as

Frits Vaandrager and Thorsten Wißmann. Action Codes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 137:1-137:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vaandrager_et_al:LIPIcs.ICALP.2023.137,
  author =	{Vaandrager, Frits and Wi{\ss}mann, Thorsten},
  title =	{{Action Codes}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{137:1--137:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.137},
  URN =		{urn:nbn:de:0030-drops-181895},
  doi =		{10.4230/LIPIcs.ICALP.2023.137},
  annote =	{Keywords: Automata, Models of Reactive Systems, LTS, Action Codes, Action Refinement, Action Contraction, Galois Connection, Model-Based Testing, Model Learning}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.38
Supported Sets - A New Foundation for Nominal Sets and Automata

Authors: Thorsten Wißmann

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
The present work proposes and discusses the category of supported sets which provides a uniform foundation for nominal sets of various kinds, such as those for equality symmetry, for the order symmetry, and renaming sets. We show that all these differently flavoured categories of nominal sets are monadic over supported sets. Thus, supported sets provide a canonical finite way to represent nominal sets and the automata therein, e.g. register automata and coalgebras in general. Name binding in supported sets is modelled by a functor following the idea of de Bruijn indices. This functor lifts to the well-known abstraction functor in nominal sets. Together with the monadicity result, this gives rise to a transformation process from finite coalgebras in supported sets to orbit-finite coalgebras in nominal sets. One instance of this process transforms the finite representation of a register automaton in supported sets into its configuration automaton in nominal sets.
Cite as

Thorsten Wißmann. Supported Sets - A New Foundation for Nominal Sets and Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{wimann:LIPIcs.CSL.2023.38,
  author =	{Wi{\ss}mann, Thorsten},
  title =	{{Supported Sets - A New Foundation for Nominal Sets and Automata}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{38:1--38:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.38},
  URN =		{urn:nbn:de:0030-drops-174992},
  doi =		{10.4230/LIPIcs.CSL.2023.38},
  annote =	{Keywords: Nominal Sets, Monads, LFP-Category, Supported Sets, Coalgebra}
}
Document
(Co)algebraic pearls
DOI: 10.4230/LIPIcs.CALCO.2021.24
Minimality Notions via Factorization Systems ((Co)algebraic pearls)

Authors: Thorsten Wißmann

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
For the minimization of state-based systems (i.e. the reduction of the number of states while retaining the system’s semantics), there are two obvious aspects: removing unnecessary states of the system and merging redundant states in the system. In the present article, we relate the two aspects on coalgebras by defining an abstract notion of minimality. The abstract notion minimality and minimization live in a general category with a factorization system. We will find criteria on the category that ensure uniqueness, existence, and functoriality of the minimization aspects. The proofs of these results instantiate to those for reachability and observability minimization in the standard coalgebra literature. Finally, we will see how the two aspects of minimization interact and under which criteria they can be sequenced in any order, like in automata minimization.
Cite as

Thorsten Wißmann. Minimality Notions via Factorization Systems ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 24:1-24:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{wimann:LIPIcs.CALCO.2021.24,
  author =	{Wi{\ss}mann, Thorsten},
  title =	{{Minimality Notions via Factorization Systems}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{24:1--24:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.24},
  URN =		{urn:nbn:de:0030-drops-153791},
  doi =		{10.4230/LIPIcs.CALCO.2021.24},
  annote =	{Keywords: Coalgebra, Reachability, Observability, Minimization, Factorization System}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.32
Explaining Behavioural Inequivalence Generically in Quasilinear Time

Authors: Thorsten Wißmann, Stefan Milius, and Lutz Schröder

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time 𝒪((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was 𝒪(m n).
Cite as

Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Explaining Behavioural Inequivalence Generically in Quasilinear Time. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{wimann_et_al:LIPIcs.CONCUR.2021.32,
  author =	{Wi{\ss}mann, Thorsten and Milius, Stefan and Schr\"{o}der, Lutz},
  title =	{{Explaining Behavioural Inequivalence Generically in Quasilinear Time}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.32},
  URN =		{urn:nbn:de:0030-drops-144094},
  doi =		{10.4230/LIPIcs.CONCUR.2021.32},
  annote =	{Keywords: bisimulation, partition refinement, modal logic, distinguishing formulae, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.28
Coalgebra Encoding for Efficient Minimization

Authors: Hans-Peter Deifel, Stefan Milius, and Thorsten Wißmann

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.
Cite as

Hans-Peter Deifel, Stefan Milius, and Thorsten Wißmann. Coalgebra Encoding for Efficient Minimization. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{deifel_et_al:LIPIcs.FSCD.2021.28,
  author =	{Deifel, Hans-Peter and Milius, Stefan and Wi{\ss}mann, Thorsten},
  title =	{{Coalgebra Encoding for Efficient Minimization}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.28},
  URN =		{urn:nbn:de:0030-drops-142664},
  doi =		{10.4230/LIPIcs.FSCD.2021.28},
  annote =	{Keywords: Coalgebra, Partition refinement, Transition systems, Minimization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.32
Efficient Coalgebraic Partition Refinement

Authors: Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in reactive verification; coalgebraic generality implies in particular that we cover not only classical relational systems but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time O(m log n) where n and m are the numbers of nodes and edges, respectively. Instances of our generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems.
Cite as

Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient Coalgebraic Partition Refinement. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dorsch_et_al:LIPIcs.CONCUR.2017.32,
  author =	{Dorsch, Ulrich and Milius, Stefan and Schr\"{o}der, Lutz and Wi{\ss}mann, Thorsten},
  title =	{{Efficient Coalgebraic Partition Refinement}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{32:1--32:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.32},
  URN =		{urn:nbn:de:0030-drops-77939},
  doi =		{10.4230/LIPIcs.CONCUR.2017.32},
  annote =	{Keywords: markov chains, deterministic finite automata, partition refinement, generic algorithm, paige-tarjan algorithm, transition systems}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.336
Finitary Corecursion for the Infinitary Lambda Calculus

Authors: Stefan Milius and Thorsten Wißmann

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

Abstract
Kurz et al. have recently shown that infinite lambda-trees with finitely many free variables modulo alpha-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational lambda-trees, i.e. those lambda-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational lambda-trees.
Cite as

Stefan Milius and Thorsten Wißmann. Finitary Corecursion for the Infinitary Lambda Calculus. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 336-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{milius_et_al:LIPIcs.CALCO.2015.336,
  author =	{Milius, Stefan and Wi{\ss}mann, Thorsten},
  title =	{{Finitary Corecursion for the Infinitary Lambda Calculus}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{336--351},
  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.336},
  URN =		{urn:nbn:de:0030-drops-55436},
  doi =		{10.4230/LIPIcs.CALCO.2015.336},
  annote =	{Keywords: rational trees, infinitary lambda calculus, coinduction}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact