19 Search Results for "Luttik, Bas"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.20
Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement

Authors: Léo Henry, Mohammad Reza Mousavi, Thomas Neele, and Matteo Sammartino

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

Abstract
Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches for concurrent systems have recently emerged. We take a significant step beyond available results, including those by the authors, and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. Our approach automatically refines the global alphabet into component alphabets while learning the component models. We develop a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets. We characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. We present a compositional learning algorithm implementing these ideas, where learning counterexamples precisely correspond to distribution counterexamples under well-defined conditions. We provide an implementation, called CoalA, using the state-of-the-art active learning library LearnLib. Our experiments show that in more than 630 subject systems, CoalA delivers orders of magnitude improvements (up to five orders) in membership queries and in systems with significant concurrency, it also achieves better scalability in the number of equivalence queries.
Cite as

Léo Henry, Mohammad Reza Mousavi, Thomas Neele, and Matteo Sammartino. Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henry_et_al:LIPIcs.CONCUR.2025.20,
  author =	{Henry, L\'{e}o and Mousavi, Mohammad Reza and Neele, Thomas and Sammartino, Matteo},
  title =	{{Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{20:1--20:22},
  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.20},
  URN =		{urn:nbn:de:0030-drops-239700},
  doi =		{10.4230/LIPIcs.CONCUR.2025.20},
  annote =	{Keywords: Active learning, Compositional methods, Concurrency theory, Labelled transition systems, Formal methods}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.17
Just Verification of Mutual Exclusion Algorithms

Authors: Rob van Glabbeek, Bas Luttik, and Myrthe S. C. Spronck

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

Abstract
We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the verification of liveness properties, it is necessary to assume a completeness criterion to eliminate spurious counterexamples. We use justness as completeness criterion. Justness depends on a concurrency relation; we consider several such relations, modelling different assumptions on the working of the shared registers. We present executions demonstrating the violation of correctness properties by several algorithms, and in some cases suggest improvements.
Cite as

Rob van Glabbeek, Bas Luttik, and Myrthe S. C. Spronck. Just Verification of Mutual Exclusion Algorithms. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 17:1-17:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanglabbeek_et_al:LIPIcs.CONCUR.2025.17,
  author =	{van Glabbeek, Rob and Luttik, Bas and Spronck, Myrthe S. C.},
  title =	{{Just Verification of Mutual Exclusion Algorithms}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{17:1--17:25},
  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.17},
  URN =		{urn:nbn:de:0030-drops-239670},
  doi =		{10.4230/LIPIcs.CONCUR.2025.17},
  annote =	{Keywords: Mutual exclusion, safe registers, regular registers, overlapping reads and writes, atomicity, safety, liveness, starvation freedom, justness, model checking, mCRL2}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.18
A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity

Authors: Jan Friso Groote and David N. Jansen

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

Abstract
We present a new O(mlog n) algorithm to calculate branching bisimulation equivalence, which is the finest commonly used behavioural equivalence on labelled transition systems that takes the internal action τ into account. This algorithm combines the simpler data structure of an earlier algorithm for Kripke structures (without action labels) with the memory-efficiency of a later algorithm partitioning sets of labelled transitions. It employs a particularly elegant four-way split of blocks of states, which refines a block under two splitters and isolates all new bottom states, simultaneously. Benchmark results show that this new algorithm outperforms the best known algorithm for branching bisimulation both in time and space.
Cite as

Jan Friso Groote and David N. Jansen. A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{groote_et_al:LIPIcs.CONCUR.2025.18,
  author =	{Groote, Jan Friso and Jansen, David N.},
  title =	{{A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{18:1--18:16},
  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.18},
  URN =		{urn:nbn:de:0030-drops-239688},
  doi =		{10.4230/LIPIcs.CONCUR.2025.18},
  annote =	{Keywords: Algorithm, Branching bisimulation, Partition refinement of states}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.35
From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases

Authors: Rowin Versteeg, Valentina Castiglioni, and Bas Luttik

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

Abstract
We consider process algebras with inaction, action prefix, non-deterministic choice and interleaving parallel composition modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum, and study the existence of finite bases (i.e., finite sound and complete axiomatisations) for these algebras. We prove that if the alphabet of actions is infinite and the behavioural equivalence is either simulation equivalence or trace equivalence, then a finite basis exists and is obtained by extending the known ground-complete axiomatisations for these behavioural equivalences. We prove that if the alphabet of actions is finite, then a finite basis does not exist for these equivalences. We also prove for all behavioural equivalences between ready simulation and completed traces there cannot exist a finite basis irrespective of the cardinality of the alphabet of actions (provided that it is non-empty). Finally, we prove that these results are maintained if the process algebra is extended with a constant for successful termination.
Cite as

Rowin Versteeg, Valentina Castiglioni, and Bas Luttik. From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{versteeg_et_al:LIPIcs.CONCUR.2025.35,
  author =	{Versteeg, Rowin and Castiglioni, Valentina and Luttik, Bas},
  title =	{{From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{35:1--35:18},
  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.35},
  URN =		{urn:nbn:de:0030-drops-239854},
  doi =		{10.4230/LIPIcs.CONCUR.2025.35},
  annote =	{Keywords: Equational basis, Parallel composition, Preorders, Equivalences, Linear time - branching time spectrum}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.26
The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum

Authors: Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir

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

Abstract
Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek’s branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become computationally hard. Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations.
Cite as

Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir. The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2025.26,
  author =	{Aceto, Luca and Achilleos, Antonis and Chalki, Aggeliki and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{26:1--26:18},
  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.26},
  URN =		{urn:nbn:de:0030-drops-227836},
  doi =		{10.4230/LIPIcs.CSL.2025.26},
  annote =	{Keywords: Characteristic formulae, prime formulae, bisimulation, simulation relations, modal logics, complexity theory, satisfiability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.38
Progress, Justness and Fairness in Modal μ-Calculus Formulae

Authors: Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
When verifying liveness properties on a transition system, it is often necessary to discard spurious violating paths by making assumptions on which paths represent realistic executions. Capturing that some property holds under such an assumption in a logical formula is challenging and error-prone, particularly in the modal μ-calculus. In this paper, we present template formulae in the modal μ-calculus that can be instantiated to a broad range of liveness properties. We consider the following assumptions: progress, justness, weak fairness, strong fairness, and hyperfairness, each with respect to actions. The correctness of these formulae has been proven.
Cite as

Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse. Progress, Justness and Fairness in Modal μ-Calculus Formulae. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 38:1-38:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{spronck_et_al:LIPIcs.CONCUR.2024.38,
  author =	{Spronck, Myrthe S. C. and Luttik, Bas and Willemse, Tim A. C.},
  title =	{{Progress, Justness and Fairness in Modal \mu-Calculus Formulae}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{38:1--38:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.38},
  URN =		{urn:nbn:de:0030-drops-208102},
  doi =		{10.4230/LIPIcs.CONCUR.2024.38},
  annote =	{Keywords: Modal \mu-calculus, Property specification, Completeness criteria, Progress, Justness, Fairness, Liveness properties}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.5
Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers

Authors: Myrthe S. C. Spronck and Bas Luttik

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We present process-algebraic models of multi-writer multi-reader safe, regular and atomic registers. We establish the relationship between our models and alternative versions presented in the literature. We use our models to formally analyse by model checking to what extent several well-known mutual exclusion algorithms are robust for relaxed atomicity requirements. Our analyses refute correctness claims made about some of these algorithms in the literature.
Cite as

Myrthe S. C. Spronck and Bas Luttik. Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{spronck_et_al:LIPIcs.CONCUR.2023.5,
  author =	{Spronck, Myrthe S. C. and Luttik, Bas},
  title =	{{Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.5},
  URN =		{urn:nbn:de:0030-drops-189995},
  doi =		{10.4230/LIPIcs.CONCUR.2023.5},
  annote =	{Keywords: mutual exclusion, model checking, non-atomic reads and writes, regular register}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.16
Typed Multi-Language Strategy Combinators

Authors: James Koppel

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Strategy combinators (also called strategic programming) are a technique for modular program transformation construction invented by Bas Luttik and Eelco Visser, best known for their instantiation in the Stratego language. Traditional implementations are dynamically typed, and struggle to represent transformations that can be usefully applied to some types, but not all. We present the design of our strategy-combinator library compstrat, a library for type-safe strategy combinators which run on Patrick Bahr’s compositional datatypes. We show how strategy combinators and compositional datatypes fuse elegantly, allowing the creation of type-preserving program transformations which operate only on datatypes satisfying certain properties. With this technique, it becomes possible to compactly define program transformations that operate on multiple programming languages. compstrat is part of the Cubix framework and has been used to build four program transformations, each of which operates on at least three languages.
Cite as

James Koppel. Typed Multi-Language Strategy Combinators. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 16:1-16:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{koppel:OASIcs.EVCS.2023.16,
  author =	{Koppel, James},
  title =	{{Typed Multi-Language Strategy Combinators}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{16:1--16:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.16},
  URN =		{urn:nbn:de:0030-drops-177865},
  doi =		{10.4230/OASIcs.EVCS.2023.16},
  annote =	{Keywords: program transformation, strategic programming}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.6
On the Axiomatisation of Branching Bisimulation Congruence over CCS

Authors: Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik

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

Abstract
In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.
Cite as

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik. On the Axiomatisation of Branching Bisimulation Congruence over CCS. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2022.6,
  author =	{Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
  title =	{{On the Axiomatisation of Branching Bisimulation Congruence over CCS}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{6:1--6: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.6},
  URN =		{urn:nbn:de:0030-drops-170692},
  doi =		{10.4230/LIPIcs.CONCUR.2022.6},
  annote =	{Keywords: Equational basis, Weak semantics, CCS, Parallel composition}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2021.8
Pushdown Automata and Context-Free Grammars in Bisimulation Semantics

Authors: Jos C. M. Baeten, Cesare Carissimo, and Bas Luttik

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

Abstract
The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings. In the Reactive Turing Machine, transitions have labels to give a notion of interactivity. In the resulting process graph, we use bisimilarity instead of language equivalence. Subsequently, we considered other classical theorems and notions from automata theory and formal languages theory. In this paper, we consider the classical theorem of the correspondence between pushdown automata and context-free grammars. By changing the process operator of sequential composition to a sequencing operator with intermediate acceptance, we get a better correspondence in our setting. We find that the missing ingredient to recover the full correspondence is the addition of a notion of state awareness.
Cite as

Jos C. M. Baeten, Cesare Carissimo, and Bas Luttik. Pushdown Automata and Context-Free Grammars in Bisimulation Semantics. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baeten_et_al:LIPIcs.CALCO.2021.8,
  author =	{Baeten, Jos C. M. and Carissimo, Cesare and Luttik, Bas},
  title =	{{Pushdown Automata and Context-Free Grammars in Bisimulation Semantics}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{8:1--8:16},
  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.8},
  URN =		{urn:nbn:de:0030-drops-153632},
  doi =		{10.4230/LIPIcs.CALCO.2021.8},
  annote =	{Keywords: pushdown automaton, context-free grammar, bisimilarity, intermediate acceptance, state awareness}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.8
Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?

Authors: Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy’s merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. This study provides a negative answer to that question based on three reasonable assumptions.
Cite as

Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2021.8,
  author =	{Aceto, Luca and Castiglioni, Valentina and Fokkink, Wan and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
  title =	{{Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.8},
  URN =		{urn:nbn:de:0030-drops-134425},
  doi =		{10.4230/LIPIcs.CSL.2021.8},
  annote =	{Keywords: Equational logic, CCS, bisimulation, parallel composition, non-finitely based algebras}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.18
On the Axiomatisability of Parallel Composition: A Journey in the Spectrum

Authors: Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.
Cite as

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen. On the Axiomatisability of Parallel Composition: A Journey in the Spectrum. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2020.18,
  author =	{Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas and Pedersen, Mathias Ruggaard},
  title =	{{On the Axiomatisability of Parallel Composition: A Journey in the Spectrum}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{18:1--18:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.18},
  URN =		{urn:nbn:de:0030-drops-128303},
  doi =		{10.4230/LIPIcs.CONCUR.2020.18},
  annote =	{Keywords: Axiomatisation, Parallel composition, Linear time-branching time spectrum}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.20
Adaptive Non-Linear Pattern Matching Automata

Authors: Rick Erkens and Maurice Laveaux

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Efficient pattern matching is fundamental for practical term rewrite engines. By preprocessing the given patterns into a finite deterministic automaton the matching patterns can be decided in a single traversal of the relevant parts of the input term. Most automaton-based techniques are restricted to linear patterns, where each variable occurs at most once, and require an additional post-processing step to check so-called variable consistency. However, we can show that interleaving the variable consistency and pattern matching phases can reduce the number of required steps to find a match all matches. Therefore, we take the existing adaptive pattern matching automata as introduced by Sekar et al and extend it these with consistency checks. We prove that the resulting deterministic pattern matching automaton is correct, and show that its evaluation depth is can be shorter than two-phase approaches.
Cite as

Rick Erkens and Maurice Laveaux. Adaptive Non-Linear Pattern Matching Automata. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{erkens_et_al:LIPIcs.FSCD.2020.20,
  author =	{Erkens, Rick and Laveaux, Maurice},
  title =	{{Adaptive Non-Linear Pattern Matching Automata}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{20:1--20:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.20},
  URN =		{urn:nbn:de:0030-drops-123427},
  doi =		{10.4230/LIPIcs.FSCD.2020.20},
  annote =	{Keywords: Pattern matching, Term indexing, Tree automata}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2019.6
An Algebraic Framework to Reason About Concurrency (Invited Talk)

Authors: Alexandra Silva

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Hoare, Struth, and collaborators proposed a concurrent extension of Kleene Algebra (CKA) as a first step towards developing algebraic reasoning for concurrent programs. Completing their research program and extending KAT to encompass concurrent behaviour has however proven to be more challenging than initially expected. The core problem appears because when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation about programs. In this talk, we will revise the literature on CKA(T) and explain the challenges and solutions in the development of an algebraic framework for concurrency. The talk is based on a series of papers joint with Tobias Kappé, Paul Brunet, Bas Luttik, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi [Tobias Kappé et al., 2017; Tobias Kappé et al., 2019; Kappé et al., 2018]. Additional references can be found on the CoNeCo project website: https://coneco-project.org/.
Cite as

Alexandra Silva. An Algebraic Framework to Reason About Concurrency (Invited Talk). In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{silva:LIPIcs.FSTTCS.2019.6,
  author =	{Silva, Alexandra},
  title =	{{An Algebraic Framework to Reason About Concurrency}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{6:1--6:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.6},
  URN =		{urn:nbn:de:0030-drops-115687},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.6},
  annote =	{Keywords: Kleene Algebra, Concurrency, Automata}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.11
Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity

Authors: Astrid Belder, Bas Luttik, and Jos Baeten

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
The Theory of Sequential Processes includes deadlock, successful termination, action prefixing, alternative and sequential composition. Intermediate acceptance, which is important for the integration of classical automata theory, can be expressed through a combination of alternative composition and successful termination. Recently, it was argued that complications arising from the interplay between intermediate acceptance and sequential composition can be eliminated by replacing sequential composition by sequencing. In this paper we study the equational theory of the recursion-free fragment of the resulting process theory modulo bisimilarity, proving that it is not finitely based, but does afford a ground-complete axiomatisation if a unary auxiliary operator is added. Furthermore, we prove that bisimilarity is decidable for processes definable by means of a finite guarded recursive specification over the process theory.
Cite as

Astrid Belder, Bas Luttik, and Jos Baeten. Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{belder_et_al:LIPIcs.CALCO.2019.11,
  author =	{Belder, Astrid and Luttik, Bas and Baeten, Jos},
  title =	{{Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{11:1--11:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.11},
  URN =		{urn:nbn:de:0030-drops-114390},
  doi =		{10.4230/LIPIcs.CALCO.2019.11},
  annote =	{Keywords: Sequencing, Sequential composition, Bisimilarity, Axiomatisation, Decidability}
}
  • Refine by Type
  • 19 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 5 2025
  • 1 2024
  • 2 2023
  • 1 2022
  • 2 2021
  • Show More...

  • Refine by Author
  • 12 Luttik, Bas
  • 4 Aceto, Luca
  • 4 Castiglioni, Valentina
  • 4 Ingólfsdóttir, Anna
  • 3 Silva, Alexandra
  • Show More...

  • Refine by Series/Journal
  • 18 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 4 Theory of computation → Equational logic and rewriting
  • 3 Theory of computation → Process calculi
  • 2 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Verification by model checking
  • 1 Software and its engineering → Formal software verification
  • Show More...

  • Refine by Keyword
  • 3 Parallel composition
  • 3 model checking
  • 2 Automata
  • 2 Axiomatisation
  • 2 CCS
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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