45 Search Results for "Nestmann, Uwe"


Volume

LIPIcs, Volume 85

28th International Conference on Concurrency Theory (CONCUR 2017)

CONCUR 2017, September 5-8, 2017, Berlin, Germany

Editors: Roland Meyer and Uwe Nestmann

Document
Inter-Blockchain Protocols with the Isabelle Infrastructure Framework

Authors: Florian Kammüller and Uwe Nestmann

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


Abstract
The main incentives of blockchain technology are distribution and distributed change, consistency, and consensus. Beyond just being a distributed ledger for digital currency, smart contracts add transaction protocols to blockchains to execute terms of a contract in a blockchain network. Inter-blockchain (IBC) protocols define and control exchanges between different blockchains. The Isabelle Infrastructure framework {has been designed to} serve security and privacy for IoT architectures by formal specification and stepwise attack analysis and refinement. A major case study of this framework is a distributed health care scenario for data consistency for GDPR compliance. This application led to the development of an abstract system specification of blockchains for IoT infrastructures. In this paper, we first give a summary of the concept of IBC. We then introduce an instantiation of the Isabelle Infrastructure framework to model blockchains. Based on this we extend this model to instantiate different blockchains and formalize IBC protocols. We prove the concept by defining the generic property of global consistency and prove it in Isabelle.

Cite as

Florian Kammüller and Uwe Nestmann. Inter-Blockchain Protocols with the Isabelle Infrastructure Framework. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{kammuller_et_al:OASIcs.FMBC.2020.11,
  author =	{Kamm\"{u}ller, Florian and Nestmann, Uwe},
  title =	{{Inter-Blockchain Protocols with the Isabelle Infrastructure Framework}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{11:1--11:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.11},
  URN =		{urn:nbn:de:0030-drops-134249},
  doi =		{10.4230/OASIcs.FMBC.2020.11},
  annote =	{Keywords: Blockchain, smart contracts, interactive theorem proving, inter-blockchain protocols}
}
Document
Complete Volume
LIPIcs, Volume 85, CONCUR'17, Complete Volume

Authors: Roland Meyer and Uwe Nestmann

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


Abstract
LIPIcs, Volume 85, CONCUR'17, Complete Volume

Cite as

28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@Proceedings{meyer_et_al:LIPIcs.CONCUR.2017,
  title =	{{LIPIcs, Volume 85, CONCUR'17, Complete Volume}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  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},
  URN =		{urn:nbn:de:0030-drops-79070},
  doi =		{10.4230/LIPIcs.CONCUR.2017},
  annote =	{Keywords: Software, Data, Theory of Computation}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Roland Meyer and Uwe Nestmann

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


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{meyer_et_al:LIPIcs.CONCUR.2017.0,
  author =	{Meyer, Roland and Nestmann, Uwe},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{0:i--0:xx},
  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.0},
  URN =		{urn:nbn:de:0030-drops-77693},
  doi =		{10.4230/LIPIcs.CONCUR.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Forward Progress on GPU Concurrency (Invited Talk)

Authors: Alastair F. Donaldson, Jeroen Ketema, Tyler Sorensen, and John Wickerson

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


Abstract
The tutorial at CONCUR will provide a practical overview of work undertaken over the last six years in the Multicore Programming Group at Imperial College London, and with collaborators internationally, related to understanding and reasoning about concurrency in software designed for acceleration on GPUs. In this article we provide an overview of this work, which includes contributions to data race analysis, compiler testing, memory model understanding and formalisation, and most recently efforts to enable portable GPU implementations of algorithms that require forward progress guarantees.

Cite as

Alastair F. Donaldson, Jeroen Ketema, Tyler Sorensen, and John Wickerson. Forward Progress on GPU Concurrency (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 1:1-1:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{donaldson_et_al:LIPIcs.CONCUR.2017.1,
  author =	{Donaldson, Alastair F. and Ketema, Jeroen and Sorensen, Tyler and Wickerson, John},
  title =	{{Forward Progress on GPU Concurrency}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{1:1--1:13},
  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.1},
  URN =		{urn:nbn:de:0030-drops-78055},
  doi =		{10.4230/LIPIcs.CONCUR.2017.1},
  annote =	{Keywords: GPUs, concurrency, formal verification, memory models, data races}
}
Document
Invited Talk
Admissibility in Games with Imperfect Information (Invited Talk)

Authors: Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur

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


Abstract
In this invited paper, we study the concept of admissible strategies for two player win/lose infinite sequential games with imperfect information. We show that in stark contrast with the perfect information variant, admissible strategies are only guaranteed to exist when players have objectives that are closed sets. As a consequence, we also study decision problems related to the existence of admissible strategies for regular games as well as finite duration games.

Cite as

Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur. Admissibility in Games with Imperfect Information (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{brenguier_et_al:LIPIcs.CONCUR.2017.2,
  author =	{Brenguier, Romain and Pauly, Arno and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{Admissibility in Games with Imperfect Information}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{2:1--2:23},
  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.2},
  URN =		{urn:nbn:de:0030-drops-78066},
  doi =		{10.4230/LIPIcs.CONCUR.2017.2},
  annote =	{Keywords: Admissibility, non-zero sum games, reactive synthesis, imperfect infor- mation}
}
Document
Invited Talk
Probabilistic Programming (Invited Talk)

Authors: Hongseok Yang

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


Abstract
Probabilistic programming refers to the idea of using standard programming constructs for specifying probabilistic models from machine learning and statistics, and employing generic inference algorithms for answering various queries on these models, such as posterior inference and estimation of model evidence. Although this idea itself is not new and was, in fact, explored by several programming-language and statistics researchers in the early 2000, it is only in the last few years that probabilistic programming has gained a large amount of attention among researchers in machine learning and programming languages, and that expressive and efficient probabilistic programming systems (such as Anglican, Church, Figaro, Infer.net, PSI, PyMC, Stan, and Venture) started to appear and have been taken up by a nontrivial number of users. The primary goal of my talk is to introduce probabilistic programming to the CONCUR/QUEST/FORMATS audience. At the end of my talk, I want the audience to understand basic results and techniques in probabilistic programming and to feel that these results and techniques are relevant or at least related to what she or he studies, although they typically come from foreign research areas, such as machine learning and statistics. My talk will contain both technical materials and lessons that I learnt from my machine-learning colleagues in Oxford, who are developing a highly-expressive higher-order probabilistic programming language, called Anglican. It will also include my work on the denotational semantics of higher-order probabilistic programming languages and their inference algorithms, which are jointly pursued with colleagues in Cambridge, Edinburgh, Oxford and Tubingen.

Cite as

Hongseok Yang. Probabilistic Programming (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{yang:LIPIcs.CONCUR.2017.3,
  author =	{Yang, Hongseok},
  title =	{{Probabilistic Programming}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{3:1--3:1},
  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.3},
  URN =		{urn:nbn:de:0030-drops-78088},
  doi =		{10.4230/LIPIcs.CONCUR.2017.3},
  annote =	{Keywords: Probabilistic programming, Machine learning, Denotational semantics}
}
Document
Invited Talk
A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk)

Authors: Azadeh Farzan and Zachary Kincaid

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


Abstract
This paper presents a high level overview of Proof Spaces [Farzan, Kincaid, and Podelski, 2015] as an instance of a new approach to compositional verification of concurrent programs and discusses potential future work extending the approach beyond its current scope of applicability.

Cite as

Azadeh Farzan and Zachary Kincaid. A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 4:1-4:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{farzan_et_al:LIPIcs.CONCUR.2017.4,
  author =	{Farzan, Azadeh and Kincaid, Zachary},
  title =	{{A New Notion of Compositionality for Concurrent Program Proofs}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{4:1--4:11},
  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.4},
  URN =		{urn:nbn:de:0030-drops-78097},
  doi =		{10.4230/LIPIcs.CONCUR.2017.4},
  annote =	{Keywords: Concurrency, Proofs, Dynamic Memory, Recursion}
}
Document
Bidirectional Nested Weighted Automata

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop

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


Abstract
Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts.

Cite as

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Bidirectional Nested Weighted Automata. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2017.5,
  author =	{Chatterjee, Krishnendu and Henzinger, Thomas A. and Otop, Jan},
  title =	{{Bidirectional Nested Weighted Automata}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{5:1--5: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.5},
  URN =		{urn:nbn:de:0030-drops-77763},
  doi =		{10.4230/LIPIcs.CONCUR.2017.5},
  annote =	{Keywords: weighted automata, nested weighted automata, complexity, bidirectional}
}
Document
k-Bounded Petri Net Synthesis from Modal Transition Systems

Authors: Uli Schlachter and Harro Wimmel

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


Abstract
We present a goal-oriented algorithm that can synthesise k-bounded Petri nets (k in N^+) from hyper modal transition systems (hMTS), an extension of labelled transition systems with optional and required behaviour. The algorithm builds a potential reachability graph of a Petri net from scratch, extending it stepwise with required behaviour from the given MTS and over-approximating the result to a new valid reachability graph. Termination occurs if either the MTS yields no additional requirements or the resulting net of the second step shows a conflict with the behaviour allowed by the MTS, making it non-sythesisable.

Cite as

Uli Schlachter and Harro Wimmel. k-Bounded Petri Net Synthesis from Modal Transition Systems. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{schlachter_et_al:LIPIcs.CONCUR.2017.6,
  author =	{Schlachter, Uli and Wimmel, Harro},
  title =	{{k-Bounded Petri Net Synthesis from Modal Transition Systems}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{6:1--6:15},
  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.6},
  URN =		{urn:nbn:de:0030-drops-77802},
  doi =		{10.4230/LIPIcs.CONCUR.2017.6},
  annote =	{Keywords: Modal transition system, bounded Petri net, synthesis}
}
Document
A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

Authors: Ki Yung Ahn, Ross Horne, and Alwen Tiu

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


Abstract
Open bisimilarity is a strong bisimulation congruence for the pi-calculus. In open bisimilarity, free names in processes are treated as variables that may be instantiated; in contrast to late bisimilarity where free names are constants. An established modal logic due to Milner, Parrow, and Walker characterises late bisimilarity, that is, two processes satisfy the same set of formulae if and only if they are bisimilar. We propose an intuitionistic variation of this modal logic and prove that it characterises open bisimilarity. The soundness proof is mechanised in Abella. The completeness proof provides an algorithm for generating distinguishing formulae, useful for explaining and certifying whenever processes are non-bisimilar.

Cite as

Ki Yung Ahn, Ross Horne, and Alwen Tiu. A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{ahn_et_al:LIPIcs.CONCUR.2017.7,
  author =	{Ahn, Ki Yung and Horne, Ross and Tiu, Alwen},
  title =	{{A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{7:1--7:17},
  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.7},
  URN =		{urn:nbn:de:0030-drops-77899},
  doi =		{10.4230/LIPIcs.CONCUR.2017.7},
  annote =	{Keywords: bisimulation, modal logic, intuitionistic logic}
}
Document
Consistently-Detecting Monitors

Authors: Adrian Francalanza

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


Abstract
We study a contextual definition for deterministic monitoring based on consistent detections. It is defined in terms of the observed behaviour of the monitor when instrumented over arbitrary systems. We give an alternative, coinductive definition based on controllability which does not rely on system quantifications, and show that it is fully-abstract with respect to the former definition. We then develop a symbolic counterpart to the controllability definition to facilitate an automated analysis for controllable monitors involving data.

Cite as

Adrian Francalanza. Consistently-Detecting Monitors. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{francalanza:LIPIcs.CONCUR.2017.8,
  author =	{Francalanza, Adrian},
  title =	{{Consistently-Detecting Monitors}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{8:1--8:19},
  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.8},
  URN =		{urn:nbn:de:0030-drops-77722},
  doi =		{10.4230/LIPIcs.CONCUR.2017.8},
  annote =	{Keywords: Runtime Monitoring, Deterministic Behaviour, Controllability, Compositional Reasoning, Symbolic Analysis}
}
Document
Flow Logic

Authors: Orna Kupferman and Gal Vardi

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


Abstract
A flow network is a directed graph in which each edge has a capacity, bounding the amount of flow that can travel through it. Flow networks have attracted a lot of research in computer science. Indeed, many questions in numerous application areas can be reduced to questions about flow networks. This includes direct applications, namely a search for a maximal flow in networks, as well as less direct applications, like maximal matching or optimal scheduling. Many of these applications would benefit from a framework in which one can formally reason about properties of flow networks that go beyond their maximal flow. We introduce Flow Logics: modal logics that treat flow functions as explicit first-order objects and enable the specification of rich properties of flow networks. The syntax of our logic BFL* (Branching Flow Logic) is similar to the syntax of the temporal logic CTL*, except that atomic assertions may be flow propositions, like > \gamma or \geq \gamma, for \gamma \in \N, which refer to the value of the flow in a vertex, and that first-order quantification can be applied both to paths and to flow functions. For example, the BFL* formula \Ef ((\geq 100) \wedge AG({\it low} \rightarrow (\leq 20)) states that there is a legal flow function in which the flow is above 100 and in all paths, the amount of flow that travels through vertices with low security is at most 20. We present an exhaustive study of the theoretical and practical aspects of BFL*, as well as extensions and fragments of it. Our extensions include flow quantifications that range over non-integral flow functions or over maximal flow functions, path quantification that ranges over paths along which non-zero flow travels, past operators, and first-order quantification of flow values. We focus on the model-checking problem and show that it is PSPACE-complete, as it is for CTL*. Handling of flow quantifiers, however, increases the complexity in terms of the network to P^{NP}, even for the LFL and BFL fragments, which are the flow-counterparts of LTL and CTL. We are still able to point to a useful fragment of BFL* for which the model-checking problem can be solved in polynomial time.

Cite as

Orna Kupferman and Gal Vardi. Flow Logic. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.CONCUR.2017.9,
  author =	{Kupferman, Orna and Vardi, Gal},
  title =	{{Flow Logic}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{9:1--9:18},
  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.9},
  URN =		{urn:nbn:de:0030-drops-77796},
  doi =		{10.4230/LIPIcs.CONCUR.2017.9},
  annote =	{Keywords: Flow Network, Temporal Logic}
}
Document
Rule Formats for Nominal Process Calculi

Authors: Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, and Yolanda Ortega-Mallén

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


Abstract
The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specification of the early pi-calculus. Our study stems from the recent Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.

Cite as

Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, and Yolanda Ortega-Mallén. Rule Formats for Nominal Process Calculi. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2017.10,
  author =	{Aceto, Luca and F\'{a}bregas, Ignacio and Garc{\'\i}a-P\'{e}rez, \'{A}lvaro and Ing\'{o}lfsd\'{o}ttir, Anna and Ortega-Mall\'{e}n, Yolanda},
  title =	{{Rule Formats for Nominal Process Calculi}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{10:1--10: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.10},
  URN =		{urn:nbn:de:0030-drops-77869},
  doi =		{10.4230/LIPIcs.CONCUR.2017.10},
  annote =	{Keywords: nominal sets, nominal structural operational semantics, process algebra, nominal transition systems, scope opening, rule formats}
}
Document
Divergence and Unique Solution of Equations

Authors: Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi

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


Abstract
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the ‘up-to techniques’). Finally, we study the theorems in name-passing calculi such as the asynchronous pi-calculus, and revisit the completeness proof of Milner’s encoding of the lambda-calculus into the pi-calculus for Lévy-Longo Trees.

Cite as

Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Divergence and Unique Solution of Equations. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{durier_et_al:LIPIcs.CONCUR.2017.11,
  author =	{Durier, Adrien and Hirschkoff, Daniel and Sangiorgi, Davide},
  title =	{{Divergence and Unique Solution of Equations}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{11:1--11: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.11},
  URN =		{urn:nbn:de:0030-drops-77849},
  doi =		{10.4230/LIPIcs.CONCUR.2017.11},
  annote =	{Keywords: Bisimilarity, unique solution of equations, termination, process calculi}
}
  • Refine by Author
  • 4 Nestmann, Uwe
  • 2 Akshay, S.
  • 2 Bonchi, Filippo
  • 2 Brunet, Paul
  • 2 Henzinger, Thomas A.
  • Show More...

  • Refine by Classification
  • 1 Networks → Peer-to-peer protocols
  • 1 Networks → Security protocols
  • 1 Software and its engineering → Software verification and validation

  • Refine by Keyword
  • 4 Concurrency
  • 2 Coverability
  • 2 Petri nets
  • 2 Process Calculi
  • 2 bisimulation
  • Show More...

  • Refine by Type
  • 44 document
  • 1 volume

  • Refine by Publication Year
  • 43 2017
  • 1 2016
  • 1 2020

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