26 Search Results for "Montanari, Ugo"


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.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
Tool Paper
CARTOGRAPHER: A Tool for String Diagrammatic Reasoning (Tool Paper)

Authors: Paweł Sobociński, Paul W. Wilson, and Fabio Zanasi

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


Abstract
We introduce cartographer, a tool for editing and rewriting string diagrams of symmetric monoidal categories. Our approach is principled: the layout exploits the isomorphism between string diagrams and certain cospans of hypergraphs; the implementation of rewriting is based on the soundness and completeness of convex double-pushout rewriting for string diagram rewriting.

Cite as

Paweł Sobociński, Paul W. Wilson, and Fabio Zanasi. CARTOGRAPHER: A Tool for String Diagrammatic Reasoning (Tool Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 20:1-20:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{sobocinski_et_al:LIPIcs.CALCO.2019.20,
  author =	{Soboci\'{n}ski, Pawe{\l} and Wilson, Paul W. and Zanasi, Fabio},
  title =	{{CARTOGRAPHER: A Tool for String Diagrammatic Reasoning}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{20:1--20:7},
  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.20},
  URN =		{urn:nbn:de:0030-drops-114482},
  doi =		{10.4230/LIPIcs.CALCO.2019.20},
  annote =	{Keywords: tool, string diagram, symmetric monoidal category, graphical reasoning}
}
Document
Translating Asynchronous Games for Distributed Synthesis

Authors: Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
In distributed synthesis, a set of process implementations is generated, which together, accomplish an objective against all possible behaviors of the environment. A lot of recent work has focussed on systems with causal memory, i.e., sets of asynchronous processes that exchange their causal histories upon synchronization. Decidability results for this problem have been stated either in terms of control games, which extend Zielonka’s asynchronous automata by partitioning the actions into controllable and uncontrollable, or in terms of Petri games, which extend Petri nets by partitioning the tokens into system and environment players. The precise connection between these two models was so far, however, an open question. In this paper, we provide the first formal connection between control games and Petri games. We establish the equivalence of the two game types based on weak bisimulations between their strategies. For both directions, we show that a game of one type can be translated into an equivalent game of the other type. We provide exponential upper and lower bounds for the translations. Our translations allow to transfer and combine decidability results between the two types of games. Exemplarily, we translate decidability in acyclic communication architectures, originally obtained for control games, to Petri games, and decidability in single-process systems, originally obtained for Petri games, to control games.

Cite as

Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch. Translating Asynchronous Games for Distributed Synthesis. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{beutner_et_al:LIPIcs.CONCUR.2019.26,
  author =	{Beutner, Raven and Finkbeiner, Bernd and Hecking-Harbusch, Jesko},
  title =	{{Translating Asynchronous Games for Distributed Synthesis}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{26:1--26:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.26},
  URN =		{urn:nbn:de:0030-drops-109289},
  doi =		{10.4230/LIPIcs.CONCUR.2019.26},
  annote =	{Keywords: synthesis, distributed systems, causal memory, Petri games, control games}
}
Document
Bialgebraic Semantics for String Diagrams

Authors: Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Turi and Plotkin’s bialgebraic semantics is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (an endofunctor). This setup is instrumental in showing that a semantic specification (a coalgebra) satisfies desirable properties: in particular, that it is compositional. In this work, we use the bialgebraic approach to derive well-behaved structural operational semantics of string diagrams, a graphical syntax that is increasingly used in the study of interacting systems across different disciplines. Our analysis relies on representing the two-dimensional operations underlying string diagrams in various categories as a monad, and their bialgebraic semantics in terms of a distributive law for that monad. As a proof of concept, we provide bialgebraic compositional semantics for a versatile string diagrammatic language which has been used to model both signal flow graphs (control theory) and Petri nets (concurrency theory). Moreover, our approach reveals a correspondence between two different interpretations of the Frobenius equations on string diagrams and two synchronisation mechanisms for processes, à la Hoare and à la Milner.

Cite as

Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Bialgebraic Semantics for String Diagrams. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2019.37,
  author =	{Bonchi, Filippo and Piedeleu, Robin and Sobocinski, Pawel and Zanasi, Fabio},
  title =	{{Bialgebraic Semantics for String Diagrams}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.37},
  URN =		{urn:nbn:de:0030-drops-109398},
  doi =		{10.4230/LIPIcs.CONCUR.2019.37},
  annote =	{Keywords: String Diagram, Structural Operational Semantics, Bialgebraic semantics}
}
Document
Revisiting the Institutional Approach to Herbrand’s Theorem

Authors: Ionut Tutu and José Luiz Fiadeiro

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


Abstract
More than a decade has passed since Herbrand’s theorem was first generalized to arbitrary institutions, enabling in this way the development of the logic-programming paradigm over formalisms beyond the conventional framework of relational first-order logic. Despite the mild assumptions of the original theory, recent developments have shown that the institution-based approach cannot capture constructions that arise when service-oriented computing is presented as a form of logic programming, thus prompting the need for a new perspective on Herbrand’s theorem founded instead upon a concept of generalized substitution system. In this paper, we formalize the connection between the institution- and the substitution-system-based approach to logic programming by investigating a number of features of institutions, like the existence of a quantification space or of representable substitutions, under which they give rise to suitable generalized substitution systems. Building on these results, we further show how the original institution independent versions of Herbrand’s theorem can be obtained as concrete instances of a more general result.

Cite as

Ionut Tutu and José Luiz Fiadeiro. Revisiting the Institutional Approach to Herbrand’s Theorem. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 304-319, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{tutu_et_al:LIPIcs.CALCO.2015.304,
  author =	{Tutu, Ionut and Fiadeiro, Jos\'{e} Luiz},
  title =	{{Revisiting the Institutional Approach to Herbrand’s Theorem}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{304--319},
  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.304},
  URN =		{urn:nbn:de:0030-drops-55419},
  doi =		{10.4230/LIPIcs.CALCO.2015.304},
  annote =	{Keywords: Institution theory, Substitution systems, Herbrand’s theorem}
}
Document
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}
}
Document
An Intensionally Fully-abstract Sheaf Model for pi

Authors: Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller

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


Abstract
Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.

Cite as

Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An Intensionally Fully-abstract Sheaf Model for pi. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 86-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{eberhart_et_al:LIPIcs.CALCO.2015.86,
  author =	{Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas},
  title =	{{An Intensionally Fully-abstract Sheaf Model for pi}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{86--100},
  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.86},
  URN =		{urn:nbn:de:0030-drops-55284},
  doi =		{10.4230/LIPIcs.CALCO.2015.86},
  annote =	{Keywords: concurrency, sheaves, causal models, games}
}
Document
Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction

Authors: Karoliina Lehtinen and Sandra Quickert

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


Abstract
We construct, for any sentence of the modal mu calculus Psi, derived sentences in the modal fragment and the fragment without least fixpoints of the modal mu calculus such that Psi is equivalent to a formula in these fragments if and only if it is equivalent to these formulas. The formula without greatest fixpoints that Psi is equivalent to if and only if it is equivalent to any formula without greatest fixpoint is obtained by duality. This yields a constructive proof of decidability of the first levels of the modal mu alternation hierarchy. The blow-up incurred by turning Psi into the modal formula is shown to be necessary: there are modal formulas that can be expressed sub-exponentially more efficiently with the use of fixpoints. For the fragments with only greatest or least fixpoints however, as long as formulas are in disjunctive form, the transformation into a formula syntactically in these fragments does not increase the size of the formula.

Cite as

Karoliina Lehtinen and Sandra Quickert. Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 457-471, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{lehtinen_et_al:LIPIcs.CSL.2015.457,
  author =	{Lehtinen, Karoliina and Quickert, Sandra},
  title =	{{Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{457--471},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.457},
  URN =		{urn:nbn:de:0030-drops-54316},
  doi =		{10.4230/LIPIcs.CSL.2015.457},
  annote =	{Keywords: modal mu calculus, fixpoint logic, alternation hierarchy}
}
Document
Relational Semantics of Linear Logic and Higher-order Model Checking

Authors: Charles Grellois and Paul-André Melliès

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


Abstract
In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higher-order recursion scheme (HORS) comes together with a dual Church encoding of an alternating tree automata (ATA) of the same signature. Moreover, the interaction between the relational interpretations of the HORS and of the ATA identifies the set of accepting states of the tree automaton against the infinite tree generated by the recursion scheme. We show how to extend this result to alternating parity automata (APT) by introducing a parametric version of the exponential modality of linear logic, capturing the formal properties of colors (or priorities) in higher-order model-checking. We show in particular how to reunderstand in this way the type-theoretic approach to higher-order model-checking developed by Kobayashi and Ong. We briefly explain in the end of the paper how this analysis driven by linear logic results in a new and purely semantic proof of decidability of the formulas of the monadic second-order logic for higher-order recursion schemes.

Cite as

Charles Grellois and Paul-André Melliès. Relational Semantics of Linear Logic and Higher-order Model Checking. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 260-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{grellois_et_al:LIPIcs.CSL.2015.260,
  author =	{Grellois, Charles and Melli\`{e}s, Paul-Andr\'{e}},
  title =	{{Relational Semantics of Linear Logic and Higher-order Model Checking}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{260--276},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.260},
  URN =		{urn:nbn:de:0030-drops-54190},
  doi =		{10.4230/LIPIcs.CSL.2015.260},
  annote =	{Keywords: Higher-order model-checking, linear logic, relational semantics, parity games, parametric comonads.}
}
Document
Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic

Authors: Matthias Baaz and Christian G. Fermüller

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


Abstract
The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.

Cite as

Matthias Baaz and Christian G. Fermüller. Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 94-109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{baaz_et_al:LIPIcs.CSL.2015.94,
  author =	{Baaz, Matthias and Ferm\"{u}ller, Christian G.},
  title =	{{Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{94--109},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.94},
  URN =		{urn:nbn:de:0030-drops-54097},
  doi =		{10.4230/LIPIcs.CSL.2015.94},
  annote =	{Keywords: Cut-elimination, sequent calculus, intuitionistic logic}
}
Document
Partial Order Reduction for Security Protocols

Authors: David Baelde, Stéphanie Delaune, and Lucca Hirschi

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g. anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. In this paper, we mitigate this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.

Cite as

David Baelde, Stéphanie Delaune, and Lucca Hirschi. Partial Order Reduction for Security Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 497-510, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.CONCUR.2015.497,
  author =	{Baelde, David and Delaune, St\'{e}phanie and Hirschi, Lucca},
  title =	{{Partial Order Reduction for Security Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{497--510},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.497},
  URN =		{urn:nbn:de:0030-drops-53946},
  doi =		{10.4230/LIPIcs.CONCUR.2015.497},
  annote =	{Keywords: Cryptographic protocols, verification, process algebra, trace equivalence}
}
Document
Modal Logics for Nominal Transition Systems

Authors: Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late and open in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.

Cite as

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal Logics for Nominal Transition Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 198-211, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{parrow_et_al:LIPIcs.CONCUR.2015.198,
  author =	{Parrow, Joachim and Borgstr\"{o}m, Johannes and Eriksson, Lars-Henrik and Gutkovas, Ramunas and Weber, Tjark},
  title =	{{Modal Logics for Nominal Transition Systems}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{198--211},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.198},
  URN =		{urn:nbn:de:0030-drops-53823},
  doi =		{10.4230/LIPIcs.CONCUR.2015.198},
  annote =	{Keywords: Process algebra, nominal sets, bisimulation, modal logic}
}
Document
A Framework for Transactional Consistency Models with Atomic Visibility

Authors: Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
Modern distributed systems often rely on databases that achieve scalability by providing only weak guarantees about the consistency of distributed transaction processing. The semantics of programs interacting with such a database depends on its consistency model, defining these guarantees. Unfortunately, consistency models are usually stated informally or using disparate formalisms, often tied to the database internals. To deal with this problem, we propose a framework for specifying a variety of consistency models for transactions uniformly and declaratively. Our specifications are given in the style of weak memory models, using structures of events and relations on them. The specifications are particularly concise because they exploit the property of atomic visibility guaranteed by many consistency models: either all or none of the updates by a transaction can be visible to another one. This allows the specifications to abstract from individual events inside transactions. We illustrate the use of our framework by specifying several existing consistency models. To validate our specifications, we prove that they are equivalent to alternative operational ones, given as algorithms closer to actual implementations. Our work provides a rigorous foundation for developing the metatheory of the novel form of concurrency arising in weakly consistent large-scale databases.

Cite as

Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 58-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{cerone_et_al:LIPIcs.CONCUR.2015.58,
  author =	{Cerone, Andrea and Bernardi, Giovanni and Gotsman, Alexey},
  title =	{{A Framework for Transactional Consistency Models with Atomic Visibility}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{58--71},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.58},
  URN =		{urn:nbn:de:0030-drops-53756},
  doi =		{10.4230/LIPIcs.CONCUR.2015.58},
  annote =	{Keywords: Replication, Consistency models, Transactions}
}
Document
05081 Abstracts Collection – Foundations of Global Computing

Authors: José Luiz Fiadeiro, Ugo Montanari, and Martin Wirsing

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)


Abstract
From 20.02.05 to 25.02.05, the Dagstuhl Seminar 05081 on ``Foundations of Global Computing'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

José Luiz Fiadeiro, Ugo Montanari, and Martin Wirsing. 05081 Abstracts Collection – Foundations of Global Computing. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{fiadeiro_et_al:DagSemProc.05081.1,
  author =	{Fiadeiro, Jos\'{e} Luiz and Montanari, Ugo and Wirsing, Martin},
  title =	{{05081 Abstracts Collection – Foundations of Global Computing}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.1},
  URN =		{urn:nbn:de:0030-drops-4590},
  doi =		{10.4230/DagSemProc.05081.1},
  annote =	{Keywords: Global Computing}
}
Document
Architectural Views for CommUnity

Authors: Cristóvão Oliveira and Michel Wermelinger

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)


Abstract
CommUnity and its categorical foundations provide a formal approach to Software Architecture (SA). Several concepts such as (re) configuration and (higher-order) connector have been given precise definitions in this setting. One of the cornerstones of the approach is the separation between computation, coordination and distribution. In this paper, we take this separation one step further and define explicit architectural views, one for each concern. They will be used to help to detect errors made while building the architecture. Moreover they will be a support to improve the design of the system by focusing on one concern at a time and/or by combining them with each other.

Cite as

Cristóvão Oliveira and Michel Wermelinger. Architectural Views for CommUnity. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:DagSemProc.05081.2,
  author =	{Oliveira, Crist\'{o}v\~{a}o and Wermelinger, Michel},
  title =	{{Architectural Views for CommUnity}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.2},
  URN =		{urn:nbn:de:0030-drops-2967},
  doi =		{10.4230/DagSemProc.05081.2},
  annote =	{Keywords: Software Architecture, views, computation, coordination, distribution}
}
  • Refine by Author
  • 4 Montanari, Ugo
  • 2 Fiadeiro, José Luiz
  • 2 König, Barbara
  • 2 Lanese, Ivan
  • 2 Sobocinski, Pawel
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Visual languages
  • 1 Theory of computation → Algorithmic game theory
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Process calculi

  • Refine by Keyword
  • 5 graph transformation
  • 3 process calculi
  • 2 bisimulation
  • 2 verification
  • 1 Anonymity
  • Show More...

  • Refine by Type
  • 26 document

  • Refine by Publication Year
  • 9 2015
  • 8 2006
  • 4 2005
  • 4 2019
  • 1 1996

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