13 Search Results for "Luttik, Bas"


Document
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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}
}
Document
Divide and Congruence III: Stability & Divergence

Authors: Wan Fokkink, Rob van Glabbeek, and Bas Luttik

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


Abstract
In two earlier papers we derived congruence formats for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. Here this work is extended with important stability and divergence requirements. Stability refers to the absence of a tau-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. Divergence, which refers to the presence of an infinite sequence of tau-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.

Cite as

Wan Fokkink, Rob van Glabbeek, and Bas Luttik. Divide and Congruence III: Stability & Divergence. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{fokkink_et_al:LIPIcs.CONCUR.2017.15,
  author =	{Fokkink, Wan and van Glabbeek, Rob and Luttik, Bas},
  title =	{{Divide and Congruence III: Stability \& Divergence}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{15:1--15: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.15},
  URN =		{urn:nbn:de:0030-drops-77855},
  doi =		{10.4230/LIPIcs.CONCUR.2017.15},
  annote =	{Keywords: Structural Operational Semantics, Compositionality, Congruence, Modal Logic, Modal Decomposition, Weak Semantics, Divergence}
}
Document
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages

Authors: Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi

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


Abstract
Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We present a new automaton model and a Kleene-like theorem that relates a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours.

Cite as

Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{kappe_et_al:LIPIcs.CONCUR.2017.25,
  author =	{Kapp\'{e}, Tobias and Brunet, Paul and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio},
  title =	{{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{25:1--25: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.25},
  URN =		{urn:nbn:de:0030-drops-77913},
  doi =		{10.4230/LIPIcs.CONCUR.2017.25},
  annote =	{Keywords: Kleene theorem, Series-rational expressions, Automata, Brzozowski derivatives, Concurrency, Pomsets}
}
Document
Invited Talk
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk)

Authors: Alexandra Silva

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)


Abstract
Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this talk will overview why the problem is so difficult. We will then pave the way towards a solution, by presenting a new automaton model and a Kleene-like theorem for CKA. More precisely, we connect a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours. We also survey how the present work can be used to to extend the network specification language NetKAT with primitives for concurrency so as to model and reason about concurrency within networks. This is joint work with Tobias Kappe, Paul Brunet, Bas Luttik, and Fabio Zanasi.

Cite as

Alexandra Silva. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{silva:LIPIcs.FSCD.2017.3,
  author =	{Silva, Alexandra},
  title =	{{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.3},
  URN =		{urn:nbn:de:0030-drops-77445},
  doi =		{10.4230/LIPIcs.FSCD.2017.3},
  annote =	{Keywords: Kleene algebras, Pomset languages, concurrency, NetKAT}
}
Document
Evidence for Fixpoint Logic

Authors: Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)


Abstract
For many modal logics, dedicated model checkers offer diagnostics (e.g., counterexamples) that help the user understand the result provided by the solver. Fixpoint logic offers a unifying framework in which such problems can be expressed and solved, but a drawback of this framework is that it lacks comprehensive diagnostics generation. We extend the framework with a notion of evidence, which can be specialized to obtain diagnostics for various model checking problems, behavioural equivalence and refinement checking problems. We demonstrate this by showing how our notion of evidence can be used to obtain diagnostics for the problem of deciding stuttering bisimilarity. Moreover, we show that our notion generalizes the existing notions of counterexample and witness for LTL and ACTL* model checking.

Cite as

Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse. Evidence for Fixpoint Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 78-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{cranen_et_al:LIPIcs.CSL.2015.78,
  author =	{Cranen, Sjoerd and Luttik, Bas and Willemse, Tim A. C.},
  title =	{{Evidence for Fixpoint Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{78--93},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.78},
  URN =		{urn:nbn:de:0030-drops-54080},
  doi =		{10.4230/LIPIcs.CSL.2015.78},
  annote =	{Keywords: fixpoint logic, diagnostics, counterexample, model checking, stuttering bisimilarity, ACTL*}
}
  • Refine by Author
  • 9 Luttik, Bas
  • 3 Aceto, Luca
  • 3 Castiglioni, Valentina
  • 3 Ingólfsdóttir, Anna
  • 3 Silva, Alexandra
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Equational logic and rewriting
  • 3 Theory of computation → Process calculi
  • 1 Software and its engineering → General programming languages
  • 1 Software and its engineering → Translator writing systems and compiler generators
  • 1 Theory of computation → Formal languages and automata theory
  • Show More...

  • Refine by Keyword
  • 2 Automata
  • 2 Axiomatisation
  • 2 CCS
  • 2 Concurrency
  • 2 Parallel composition
  • Show More...

  • Refine by Type
  • 13 document

  • Refine by Publication Year
  • 3 2017
  • 2 2019
  • 2 2020
  • 2 2021
  • 2 2023
  • Show More...

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