Volume
LIPIcs, Volume 42
26th International Conference on Concurrency Theory (CONCUR 2015)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
CONCUR 2015, September 1-4, 2015, Madrid, SpainEditors
Publication Details
- published at: 2015-08-26
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-91-0
- DBLP: db/conf/concur/concur2015
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 42, CONCUR'15, Complete Volume
Abstract
LIPIcs, Volume 42, CONCUR'15, Complete Volume
Cite as
26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{aceto_et_al:LIPIcs.CONCUR.2015,
title = {{LIPIcs, Volume 42, CONCUR'15, Complete Volume}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
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},
URN = {urn:nbn:de:0030-drops-54628},
doi = {10.4230/LIPIcs.CONCUR.2015},
annote = {Keywords: Computer-Communication Networks, Software Engineering, Computation by Abstract Devices, Logics and Meanings of Programs, Simulation and Modeling}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Committees, External Reviewers
Abstract
Front Matter, Table of Contents, Preface, Committees, External Reviewers
Cite as
26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2015.i,
author = {Aceto, Luca and de Frutos Escrig, David},
title = {{Front Matter, Table of Contents, Preface, Committees, External Reviewers}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {i--xiv},
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.i},
URN = {urn:nbn:de:0030-drops-53610},
doi = {10.4230/LIPIcs.CONCUR.2015.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, Committees, External Reviewers}
}
Document
Invited Paper
Automatic Application Deployment in the Cloud: from Practice to Theory and Back (Invited Paper)
Abstract
The problem of deploying a complex software application has been formally investigated in previous work by means of the abstract component model named Aeolus. As the problem turned out to be undecidable, simplified versions of the model were investigated in which decidability was restored by introducing limitations on the ways components are described.
In this paper, we take an opposite approach, and investigate the possibility to address a relaxed version of the deployment
problem without limiting the expressiveness of the component model. We identify three problems to be solved in sequence: (i) the verification of the existence of a final configuration in which all the constraints imposed by the single components are satisfied, (ii) the generation of a concrete configuration satisfying such constraints, and (iii) the synthesis of a plan to reach such a configuration possibly going through intermediary configurations that violate the non-functional constraints.
Cite as
Roberto Di Cosmo, Michael Lienhardt, Jacopo Mauro, Stefano Zacchiroli, Gianluigi Zavattaro, and Jakub Zwolakowski. Automatic Application Deployment in the Cloud: from Practice to Theory and Back (Invited Paper). In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{dicosmo_et_al:LIPIcs.CONCUR.2015.1,
author = {Di Cosmo, Roberto and Lienhardt, Michael and Mauro, Jacopo and Zacchiroli, Stefano and Zavattaro, Gianluigi and Zwolakowski, Jakub},
title = {{Automatic Application Deployment in the Cloud: from Practice to Theory and Back}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {1--16},
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.1},
URN = {urn:nbn:de:0030-drops-53956},
doi = {10.4230/LIPIcs.CONCUR.2015.1},
annote = {Keywords: Automatic deployment, Planning, DevOps, Constraint Programming}
}
Document
Invited Paper
Reachability Problems for Continuous Linear Dynamical Systems (Invited Paper)
Abstract
It is well understood that the interaction between discrete and continuous dynamics makes hybrid automata difficult to analyse algorithmically. However it is already the case that many natural verification questions concerning only the continuous dynamics of such systems are extremely challenging. This remains so even for linear dynamical systems, such as linear hybrid automata and continuous-time Markov chains, whose evolution is detemined by linear differential equations. For example, one can ask to decide whether it is possible to escape a particular location of a linear hybrid automaton, given initial values of the continuous variables. Likewise one can ask whether a given set of probability distributions is reachable during the evolution of continuous-time Markov chain.
This talk focusses on reachability problems for solutions of linear differential equations. A central decision problem in this area is the Continuous Skolem Problem, which asks whether a real-valued function satisfying an ordinary linear differential equation has a zero. This can be seen as a continuous analog of the Skolem Problem for linear recurrence sequences, which asks whether the sequence satisfying a given recurrence has a zero term. For both the discrete and continuous versions of the Skolem Problem, decidability is open.
We show that the Continuous Skolem Problem lies at the heart of many natural verification questions on linear dynamical systems. We describe some recent work, done in collaboration with Chonev and Ouaknine, that uses results in transcendence theory and real algebraic geometry to obtain decidability for certain variants of the problem. In particular, we consider a bounded version of the Continuous Skolem Problem, corresponding to time-bounded reachability. We prove decidability of the bounded problem assuming Schanuel's conjecture, one of the main conjectures in transcendence theory. We describe some partial decidability results in the unbounded case and discuss mathematical obstacles to proving decidability of the Continuous Skolem Problem in full generality.
Cite as
James Worrell. Reachability Problems for Continuous Linear Dynamical Systems (Invited Paper). In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, p. 17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{worrell:LIPIcs.CONCUR.2015.17,
author = {Worrell, James},
title = {{Reachability Problems for Continuous Linear Dynamical Systems}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {17--17},
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.17},
URN = {urn:nbn:de:0030-drops-53960},
doi = {10.4230/LIPIcs.CONCUR.2015.17},
annote = {Keywords: Linear differential Equations, Hybrid Automata, Schanuel's Conjecture}
}
Document
Invited Paper
Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap (Invited Paper)
Abstract
We review and compare three notions of conformance testing for cyber-physical systems. We begin with a review of their underlying semantic models and present conformance-preserving translations between them. We identify the differences in the underlying semantic models and the various design decisions that lead to these substantially different notions of conformance testing. Learning from this exercise, we reflect upon the challenges in designing an "ideal" notion of conformance for cyber-physical systems and sketch a roadmap of future research in this domain.
Cite as
Narges Khakpour and Mohammad Reza Mousavi. Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap (Invited Paper). In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 18-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{khakpour_et_al:LIPIcs.CONCUR.2015.18,
author = {Khakpour, Narges and Mousavi, Mohammad Reza},
title = {{Notions of Conformance Testing for Cyber-Physical Systems: Overview and Roadmap}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {18--40},
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.18},
URN = {urn:nbn:de:0030-drops-53975},
doi = {10.4230/LIPIcs.CONCUR.2015.18},
annote = {Keywords: Cyber-physical systems, hybrid systems, conformance testing, model-based testing, behavioral pre-orders, hybrid input-output conformance testing, (tau}
}
Document
Invited Paper
Behavioural Equivalences for Co-operating Transactions (Invited Paper)
Abstract
Relaxing the isolation requirements on transactions leads to systems in which transactions can now co-operate to achieve distributed goals. However in the absence of isolation it is not easy to understand the desired behaviour of transactional systems, or the extent to which the other standard ACID properties of transactions can be maintained: atomicity, consistency and durability. In this talk I will give an overview of some recent work in this area, outlining semantic theories for a process calculus which has been augmented by a new construct for co-operating transactions.
Cite as
Matthew Hennessy. Behavioural Equivalences for Co-operating Transactions (Invited Paper). In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, p. 41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hennessy:LIPIcs.CONCUR.2015.41,
author = {Hennessy, Matthew},
title = {{Behavioural Equivalences for Co-operating Transactions}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {41--41},
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.41},
URN = {urn:nbn:de:0030-drops-53985},
doi = {10.4230/LIPIcs.CONCUR.2015.41},
annote = {Keywords: Behavioural equivalences, transactional systems}
}
Document
Invited Paper
Applications of Automata and Concurrency Theory in Networks (Invited Paper)
Abstract
Networks have received widespread attention in recent years as a target for domain-specific language design. The emergence of software-defined networking (SDN) as a popular paradigm for network programming has led to the appearance of a number of SDN programming languages seeking to provide high-level abstractions to simplify the task of specifying the packet-processing behavior of a network.
Previous work by Anderson et al. [Anderson et al.,POPL'14,2014] introduced NetKAT, a language and logic for specifying and verifying the packet-processing behavior of networks. NetKAT provides general-purpose programming constructs such as parallel and sequential composition, conditional tests, and iteration, as well as special-purpose primitives for querying and modifying packet headers and encoding network topologies. In contrast to competing approaches, NetKAT has a formal mathematical semantics and an equational deductive system that is sound and complete over that semantics, as well as a PSPACE decision procedure. It is based on Kleene algebra with tests (KAT), an algebraic system for propositional program verification that has been extensively studied for nearly two decades [Kozen,ACM Trans. Program. Lang. Syst.,1997]. Several practical applications of NetKAT have been developed, including algorithms for testing reachability and non-interference and a syntactic correctness proof for a compiler that translates programs to hardware instructions for SDN switches.
In a follow-up paper [Foster et al.,POPL'15,2015], the coalgebraic theory of NetKAT was developed and a bisimulation-based algorithm for deciding equivalence was devised. The new algorithm was shown to be significantly more efficient than the previous naive algorithm [Anderson et al.,POPL'14,2014], which was PSPACE in the best case and the worst case, as it was based on the determinization of a nondeterministic algorithm. Along with the coalgebraic model of NetKAT, the authors presented a specialized version of the Brzozowski derivative in both semantic and syntactic forms. They also also proved a version of Kleene's theorem for NetKAT that shows that the coalgebraic model is equivalent to the standard packet-processing and language models introduced previously [Anderson et al.,POPL'14,2014]. They demonstrated the real-world applicability of the tool by using it to decide common network verification questions such as all-pairs connectivity, loop-freedom, and translation validation - all pressing questions in modern networks.
This talk will survey applications of automata theory, concurrency theory and coalgebra to problems in networking. We will suggest directions for exploring the bridge between the two communities and ways to deliver new synergies. On the one hand, this will lead to new insights and techniques that will enable the development of rigorous semantic foundations for networks. On the other hand, the idysiocransies of networks will provide new challenges for the automata and concurrency community.
Cite as
Alexandra Silva. Applications of Automata and Concurrency Theory in Networks (Invited Paper). In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 42-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{silva:LIPIcs.CONCUR.2015.42,
author = {Silva, Alexandra},
title = {{Applications of Automata and Concurrency Theory in Networks}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {42--43},
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.42},
URN = {urn:nbn:de:0030-drops-53993},
doi = {10.4230/LIPIcs.CONCUR.2015.42},
annote = {Keywords: Automata, network programming, coalgebra}
}
Document
Distributed Local Strategies in Broadcast Networks
Abstract
We study the problems of reaching a specific control state, or converging to a set of target states, in networks with a parameterized number of identical processes communicating via broadcast. To reflect the distributed aspect of such networks, we restrict our attention to executions in which all the processes must follow the same local strategy that, given their past performed actions and received messages, provides the next action to be performed. We show that the reachability and target problems under such local strategies are NP-complete, assuming that the set of receivers is chosen non-deterministically at each step. On the other hand, these problems become undecidable when the communication topology is a clique. However, decidability can be regained for reachability under the additional assumption that all processes are bound to receive the broadcast messages.
Cite as
Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Distributed Local Strategies in Broadcast Networks. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 44-57, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2015.44,
author = {Bertrand, Nathalie and Fournier, Paulin and Sangnier, Arnaud},
title = {{Distributed Local Strategies in Broadcast Networks}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {44--57},
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.44},
URN = {urn:nbn:de:0030-drops-53796},
doi = {10.4230/LIPIcs.CONCUR.2015.44},
annote = {Keywords: Broadcast networks, parameterized verification, local strategies}
}
Document
A Framework for Transactional Consistency Models with Atomic Visibility
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
Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
Abstract
Verification of concurrent systems is a difficult problem in general, and this is the case even more in a parametrized setting where unboundedly many concurrent components are considered. Recently, Hague proposed an architecture with a leader process and unboundedly many copies of a contributor process interacting over a shared memory for which safety properties can be effectively verified. All processes in Hague's setting are pushdown automata. Here, we extend it by considering other formal models and, as a main contribution, find very liberal conditions on the individual processes under which the safety problem is decidable: the only substantial condition we require is the effective computability of the downward closure for the class of the leader processes. Furthermore, our result allows for a hierarchical approach to constructing models of concurrent systems with decidable safety problem: networks with tree-like architecture, where each process shares a register with its children processes (and another register with its parent). Nodes in such networks can be for instance pushdown automata, Petri nets, or multi-pushdown systems with decidable reachability problem.
Cite as
Salvatore La Torre, Anca Muscholl, and Igor Walukiewicz. Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 72-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{latorre_et_al:LIPIcs.CONCUR.2015.72,
author = {La Torre, Salvatore and Muscholl, Anca and Walukiewicz, Igor},
title = {{Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {72--84},
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.72},
URN = {urn:nbn:de:0030-drops-53813},
doi = {10.4230/LIPIcs.CONCUR.2015.72},
annote = {Keywords: Verification, parametrized systems, shared memory}
}
Document
On the Succinctness of Idioms for Concurrent Programming
Abstract
The ability to create succinct programs is a central criterion for comparing programming and specification methods. Specifically, approaches to concurrent programming can often be thought of as idioms for the composition of automata, and as such they can then be compared using the standard and natural measure for the complexity of automata, descriptive succinctness. This measure captures the size of the automata that the evaluated approach needs for expressing the languages under discussion. The significance of this metric lies, among other things, in its impact on software reliability, maintainability, reusability and simplicity, and on software analysis and verification. Here, we focus on the succinctness afforded by three basic concurrent programming idioms: requesting events, blocking events and waiting for events. We show that a programming model containing all three idioms is exponentially more succinct than non-parallel automata, and that its succinctness is additive to that of classical nondeterministic and "and" automata. We also show that our model is strictly contained in the model of cooperating automata à la statecharts, but that it may provide similar exponential succinctness over non-parallel automata as the more general model - while affording increased encapsulation. We then investigate the contribution of each of the three idioms to the descriptive succinctness of the model as a whole, and show that they each have their unique succinctness advantages that are not subsumed by their counterparts. Our results contribute to a rigorous basis for assessing the complexity of specifying, developing and maintaining complex concurrent software.
Cite as
David Harel, Guy Katz, Robby Lampert, Assaf Marron, and Gera Weiss. On the Succinctness of Idioms for Concurrent Programming. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 85-99, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{harel_et_al:LIPIcs.CONCUR.2015.85,
author = {Harel, David and Katz, Guy and Lampert, Robby and Marron, Assaf and Weiss, Gera},
title = {{On the Succinctness of Idioms for Concurrent Programming}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {85--99},
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.85},
URN = {urn:nbn:de:0030-drops-53849},
doi = {10.4230/LIPIcs.CONCUR.2015.85},
annote = {Keywords: Descriptive Succinctness, Module Size, Automata, Bounded Concurrency}
}
Document
Assume-Admissible Synthesis
Abstract
In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. It is based on the notion of admissible strategies. We compare our novel rule with previous rules defined in the literature, and we show that contrary to the previous proposals, our rule define sets of solutions which are rectangular. This property leads to solutions which are robust and resilient. We provide algorithms with optimal complexity and also an abstraction framework.
Cite as
Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-Admissible Synthesis. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 100-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{brenguier_et_al:LIPIcs.CONCUR.2015.100,
author = {Brenguier, Romain and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
title = {{Assume-Admissible Synthesis}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {100--113},
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.100},
URN = {urn:nbn:de:0030-drops-53711},
doi = {10.4230/LIPIcs.CONCUR.2015.100},
annote = {Keywords: Multi-player games, controller synthesis, admissibility}
}
Document
Reactive Synthesis Without Regret
Abstract
Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies, and show that the two last cases have natural modelling applications. We also show that our notion of regret minimization in which Adam is limited to word strategies generalizes the notion of good for games introduced by Henzinger and Piterman, and is related to the notion of determinization by pruning due to Aminof, Kupferman and Lampert.
Cite as
Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive Synthesis Without Regret. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 114-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hunter_et_al:LIPIcs.CONCUR.2015.114,
author = {Hunter, Paul and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
title = {{Reactive Synthesis Without Regret}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {114--127},
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.114},
URN = {urn:nbn:de:0030-drops-53675},
doi = {10.4230/LIPIcs.CONCUR.2015.114},
annote = {Keywords: Quantitative games, regret, verification, synthesis, game theory}
}
Document
Synthesis of Bounded Choice-Free Petri Nets
Abstract
This paper describes a synthesis algorithm tailored to the construction of choice-free Petri nets from finite persistent transition systems. With this goal in mind, a minimised set of simplified systems of linear inequalities is distilled from a general region-theoretic approach, leading to algorithmic improvements as well as to a partial characterisation of the class of persistent transition systems that have a choice-free Petri net realisation.
Cite as
Eike Best and Raymond Devillers. Synthesis of Bounded Choice-Free Petri Nets. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 128-141, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{best_et_al:LIPIcs.CONCUR.2015.128,
author = {Best, Eike and Devillers, Raymond},
title = {{Synthesis of Bounded Choice-Free Petri Nets}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {128--141},
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.128},
URN = {urn:nbn:de:0030-drops-53853},
doi = {10.4230/LIPIcs.CONCUR.2015.128},
annote = {Keywords: Choice-freeness, labelled transition systems, persistence, Petri nets, system synthesis}
}
Document
Polynomial Time Decidability of Weighted Synchronization under Partial Observability
Abstract
We consider weighted automata with both positive and negative integer weights on edges and study the problem of synchronization using adaptive strategies that may only observe whether the current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.
Cite as
Jan Kretinsky, Kim Guldstrand Larsen, Simon Laursen, and Jiri Srba. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 142-154, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2015.142,
author = {Kretinsky, Jan and Larsen, Kim Guldstrand and Laursen, Simon and Srba, Jiri},
title = {{Polynomial Time Decidability of Weighted Synchronization under Partial Observability}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {142--154},
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.142},
URN = {urn:nbn:de:0030-drops-53927},
doi = {10.4230/LIPIcs.CONCUR.2015.142},
annote = {Keywords: weighted automata, partial observability, synchronization, complexity}
}
Document
SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators
Abstract
Compositional reasoning over probabilistic systems wrt. behavioral metric semantics requires the language operators to be uniformly continuous. We study which SOS specifications define uniformly continuous operators wrt. bisimulation metric semantics. We propose an expressive specification format that allows us to specify operators of any given modulus of continuity. Moreover, we provide a method that allows to derive from any given specification the modulus of continuity of its operators.
Cite as
Daniel Gebler and Simone Tini. SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 155-168, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{gebler_et_al:LIPIcs.CONCUR.2015.155,
author = {Gebler, Daniel and Tini, Simone},
title = {{SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {155--168},
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.155},
URN = {urn:nbn:de:0030-drops-53876},
doi = {10.4230/LIPIcs.CONCUR.2015.155},
annote = {Keywords: SOS, probabilistic process algebra, bisimulation metric semantics, compositional metric reasoning, uniform continuity}
}
Document
Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes
Abstract
We study the problem of finite-horizon probabilistic invariance for discrete-time Markov processes over general (uncountable) state spaces. We compute discrete-time, finite-state Markov chains as formal abstractions of general Markov processes. Our abstraction differs from existing approaches in two ways. First, we exploit the structure of the underlying Markov process to compute the abstraction separately for each dimension. Second, we employ dynamic Bayesian networks (DBN) as compact representations of the abstraction. In contrast, existing approaches represent and store the (exponentially large) Markov chain explicitly, which leads to heavy memory requirements limiting the application to models of dimension less than half, according to our experiments.
We show how to construct a DBN abstraction of a Markov process satisfying an independence assumption on the driving process noise. We compute a guaranteed bound on the error in the abstraction w.r.t. the probabilistic invariance property; the dimension-dependent abstraction makes the error bounds more precise than existing approaches. Additionally, we show how factor graphs and the sum-product algorithm for DBNs can be used to solve the finite-horizon probabilistic invariance problem. Together, DBN-based representations and algorithms can be significantly more efficient than explicit representations of Markov chains for abstracting and model checking structured Markov processes.
Cite as
Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar. Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 169-183, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{esmaeilzadehsoudjani_et_al:LIPIcs.CONCUR.2015.169,
author = {Esmaeil Zadeh Soudjani, Sadegh and Abate, Alessandro and Majumdar, Rupak},
title = {{Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {169--183},
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.169},
URN = {urn:nbn:de:0030-drops-53693},
doi = {10.4230/LIPIcs.CONCUR.2015.169},
annote = {Keywords: Structured stochastic systems, general space Markov processes, formal verification, dynamic Bayesian networks, Markov chain abstraction}
}
Document
On Frequency LTL in Probabilistic Systems
Abstract
We study frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator G^p expressing that on a path, certain formula holds with at least a given frequency p, thus relaxing the semantics of the usual G operator of LTL. Such logic is particularly useful in probabilistic systems, where some undesirable events such as random failures may occur and are acceptable if they are rare enough. Frequency-related extensions of LTL have been previously studied by several authors, where mostly the logic is equipped with an extended "until" and "globally" operator, leading to undecidability of most interesting problems.
For the variant we study, we are able to establish fundamental decidability results. We show that for Markov chains, the problem of computing the probability with which a given fLTL formula holds has the same complexity as the analogous problem for LTL. We also show that for Markov decision processes the problem becomes more delicate, but when restricting the frequency bound p to be 1 and negations not to be outside any G^p operator, we can compute the maximum probability of satisfying the fLTL formula. This can be again performed with the same time complexity as for the ordinary LTL formulas.
Cite as
Vojtech Forejt and Jan Krcal. On Frequency LTL in Probabilistic Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 184-197, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{forejt_et_al:LIPIcs.CONCUR.2015.184,
author = {Forejt, Vojtech and Krcal, Jan},
title = {{On Frequency LTL in Probabilistic Systems}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {184--197},
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.184},
URN = {urn:nbn:de:0030-drops-53789},
doi = {10.4230/LIPIcs.CONCUR.2015.184},
annote = {Keywords: Markov chains, Markov decision processes, LTL, controller synthesis}
}
Document
Modal Logics for Nominal Transition Systems
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
Howe's Method for Contextual Semantics
Abstract
We show how to use Howe's method to prove that context bisimilarity is a congruence for process calculi equipped with their usual semantics. We apply the method to two extensions of HOpi, with passivation and with join patterns, illustrating different proof techniques.
Cite as
Serguei Lenglet and Alan Schmitt. Howe's Method for Contextual Semantics. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 212-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{lenglet_et_al:LIPIcs.CONCUR.2015.212,
author = {Lenglet, Serguei and Schmitt, Alan},
title = {{Howe's Method for Contextual Semantics}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {212--225},
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.212},
URN = {urn:nbn:de:0030-drops-53642},
doi = {10.4230/LIPIcs.CONCUR.2015.212},
annote = {Keywords: Bisimulation, process calculi, Howe's method}
}
Document
Forward and Backward Bisimulations for Chemical Reaction Networks
Abstract
We present two quantitative behavioral equivalences over species of a chemical reaction network (CRN) with semantics based on ordinary differential equations. Forward CRN bisimulation identifies a partition where each equivalence class represents the exact sum of the concentrations of the species belonging to that class. Backward CRN bisimulation relates species that have identical solutions at all time points when starting from the same initial conditions. Both notions can be checked using only CRN syntactical information, i.e., by inspection of the set of reactions. We provide a unified algorithm that computes the coarsest refinement up to our bisimulations in polynomial time. Further, we give algorithms to compute quotient CRNs induced by a bisimulation. As an application, we find significant reductions in a number of models of biological processes from the literature. In two cases we allow the analysis of benchmark models which would be otherwise intractable due to their memory requirements.
Cite as
Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin. Forward and Backward Bisimulations for Chemical Reaction Networks. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 226-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{cardelli_et_al:LIPIcs.CONCUR.2015.226,
author = {Cardelli, Luca and Tribastone, Mirco and Tschaikowski, Max and Vandin, Andrea},
title = {{Forward and Backward Bisimulations for Chemical Reaction Networks}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {226--239},
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.226},
URN = {urn:nbn:de:0030-drops-53684},
doi = {10.4230/LIPIcs.CONCUR.2015.226},
annote = {Keywords: Chemical reaction networks, ordinary differential equations, bisimulation, partition refinement}
}
Document
Lax Bialgebras and Up-To Techniques for Weak Bisimulations
Abstract
Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras. In this paper, we prove the soundness of up-to contextual closure for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend our previously developed categorical framework to an ordered setting.
Cite as
Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 240-253, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2015.240,
author = {Bonchi, Filippo and Petrisan, Daniela and Pous, Damien and Rot, Jurriaan},
title = {{Lax Bialgebras and Up-To Techniques for Weak Bisimulations}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {240--253},
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.240},
URN = {urn:nbn:de:0030-drops-53709},
doi = {10.4230/LIPIcs.CONCUR.2015.240},
annote = {Keywords: Up-to techniques, weak bisimulation, (lax) bialgebras}
}
Document
On the Satisfiability of Indexed Linear Temporal Logics
Abstract
Indexed Linear Temporal Logics (ILTL) are an extension of standard Linear Temporal Logics (LTL) with quantifications over index variables which range over a set of process identifiers. ILTL has been widely used in specifying and verifying properties of parameterised systems, e.g., in parameterised model checking of concurrent processes. However there is still a lack of theoretical investigations on properties of ILTL, compared to the well-studied LTL. In this paper, we start to narrow this gap, focusing on the satisfiability problem, i.e., to decide whether a model exists for a given formula. This problem is in general undecidable. Various fragments of ILTL have been considered in the literature typically in parameterised model checking, e.g., ILTL formulae in prenex normal form, or containing only non-nested quantifiers, or admitting limited temporal operators. We carry out a thorough study on the decidability and complexity of the satisfiability problem for these fragments. Namely, for each fragment, we either show that it is undecidable, or otherwise provide tight complexity bounds.
Cite as
Taolue Chen, Fu Song, and Zhilin Wu. On the Satisfiability of Indexed Linear Temporal Logics. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 254-267, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CONCUR.2015.254,
author = {Chen, Taolue and Song, Fu and Wu, Zhilin},
title = {{On the Satisfiability of Indexed Linear Temporal Logics}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {254--267},
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.254},
URN = {urn:nbn:de:0030-drops-53767},
doi = {10.4230/LIPIcs.CONCUR.2015.254},
annote = {Keywords: Satisfiability, Indexed linear temporal logic, Parameterised systems}
}
Document
Expresiveness and Complexity Results for Strategic Reasoning
Abstract
This paper presents a range of expressiveness and complexity results for the specification, computation, and verification of Nash equilibria in multi-player non-zero-sum concurrent games in which players have goals expressed as temporal logic formulae. Our results are based on a novel approach to the characterisation of equilibria in such games: a semantic characterisation based on winning strategies and memoryful reasoning. This characterisation allows us to obtain a number of other results relating to the analysis of equilibrium properties in temporal logic.
We show that, up to bisimilarity, reasoning about Nash equilibria in multi-player non-zero-sum concurrent games can be done in ATL^* and that constructing equilibrium strategy profiles in such games can be done in 2EXPTIME using finite-memory strategies. We also study two simpler cases, two-player games and sequential games, and show that the specification of equilibria in the latter setting can be obtained in a temporal logic that is weaker than ATL^*. Based on these results, we settle a few open problems, put forward new logical characterisations of equilibria, and provide improved answers and alternative solutions to a number of questions.
Cite as
Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. Expresiveness and Complexity Results for Strategic Reasoning. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 268-282, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{gutierrez_et_al:LIPIcs.CONCUR.2015.268,
author = {Gutierrez, Julian and Harrenstein, Paul and Wooldridge, Michael},
title = {{Expresiveness and Complexity Results for Strategic Reasoning}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {268--282},
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.268},
URN = {urn:nbn:de:0030-drops-53802},
doi = {10.4230/LIPIcs.CONCUR.2015.268},
annote = {Keywords: Temporal logic, Nash equilibrium, game models, formal verification}
}
Document
Meeting Deadlines Together
Abstract
This paper studies safety, progress, and non-zeno properties of Communicating Timed Automata (CTAs), which are timed automata (TA) extended with unbounded communication channels, and presents a procedure to build timed global specifications from systems of CTAs. We define safety and progress properties for CTAs by extending properties studied in communicating finite-state machines to the timed setting. We then study non-zenoness for CTAs; our aim is to prevent scenarios in which the participants have to execute an infinite number of actions in a finite amount of time. We propose sound and decidable conditions for these properties, and demonstrate the practicality of our approach with an implementation and experimental evaluations of our theory.
Cite as
Laura Bocchi, Julien Lange, and Nobuko Yoshida. Meeting Deadlines Together. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 283-296, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bocchi_et_al:LIPIcs.CONCUR.2015.283,
author = {Bocchi, Laura and Lange, Julien and Yoshida, Nobuko},
title = {{Meeting Deadlines Together}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {283--296},
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.283},
URN = {urn:nbn:de:0030-drops-53838},
doi = {10.4230/LIPIcs.CONCUR.2015.283},
annote = {Keywords: timed automata, multiparty session types, global specification}
}
Document
To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games
Abstract
Quantitative games are two-player zero-sum games played on directed weighted graphs. Total-payoff games - that can be seen as a refinement of the well-studied mean-payoff games - are the variant where the payoff of a play is computed as the sum of the weights. Our aim is to describe the first pseudo-polynomial time algorithm for total-payoff games in the presence of arbitrary weights. It consists of a non-trivial application of the value iteration paradigm. Indeed, it requires to study, as a milestone, a refinement of these games, called min-cost reachability games, where we add a reachability objective to one of the players. For these games, we give an efficient value iteration algorithm to compute the values and optimal strategies (when they exist), that runs in pseudo-polynomial time. We also propose heuristics to speed up the computations.
Cite as
Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 297-310, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2015.297,
author = {Brihaye, Thomas and Geeraerts, Gilles and Haddad, Axel and Monmege, Benjamin},
title = {{To Reach or not to Reach? Efficient Algorithms for Total-Payoff Games}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {297--310},
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.297},
URN = {urn:nbn:de:0030-drops-53729},
doi = {10.4230/LIPIcs.CONCUR.2015.297},
annote = {Keywords: Games on graphs, reachability, quantitative games, value iteration}
}
Document
On the Value Problem in Weighted Timed Games
Abstract
A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question, which has already been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been identified for which optimal weight and almost-optimal strategies can be computed. In this paper, we show that the value problem is undecidable in weighted timed games. We then introduce a large subclass of weighted timed games (for which the undecidability proof above applies), and provide an algorithm to compute arbitrary approximations of the value in such games. To the best of our knowledge, this is the first approximation scheme for an undecidable class of weighted timed games.
Cite as
Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the Value Problem in Weighted Timed Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 311-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2015.311,
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {{On the Value Problem in Weighted Timed Games}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {311--324},
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.311},
URN = {urn:nbn:de:0030-drops-53863},
doi = {10.4230/LIPIcs.CONCUR.2015.311},
annote = {Keywords: Timed games, undecidability, approximation}
}
Document
Repairing Multi-Player Games
Abstract
Synthesis is the automated construction of systems from their specifications. Modern systems often consist of interacting components, each having its own objective. The interaction among the components is modeled by a multi-player game. Strategies of the components induce a trace in the game, and the objective of each component is to force the game into a trace that satisfies its specification. This is modeled by augmenting the game with omega-regular winning conditions. Unlike traditional synthesis games, which are zero-sum, here the objectives of the components do not necessarily contradict each other. Accordingly, typical questions about these games concern their stability - whether the players reach an equilibrium, and their social welfare - maximizing the set of (possibly weighted) specifications that are satisfied.
We introduce and study repair of multi-player games. Given a game, we study the possibility of modifying the objectives of the players in order to obtain stability or to improve the social welfare. Specifically, we solve the problem of modifying the winning conditions in a given concurrent multi-player game in a way that guarantees the existence of a Nash equilibrium. Each modification has a value, reflecting both the cost of strengthening or weakening the underlying specifications, as well as the benefit of satisfying specifications in the obtained equilibrium. We seek optimal modifications, and we study the problem for various omega-regular objectives and various cost and benefit functions. We analyze the complexity of the problem in the general setting as well as in one with a fixed number of players. We also study two additional types of repair, namely redirection of transitions and control of a subset of the players.
Cite as
Shaull Almagor, Guy Avni, and Orna Kupferman. Repairing Multi-Player Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 325-339, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CONCUR.2015.325,
author = {Almagor, Shaull and Avni, Guy and Kupferman, Orna},
title = {{Repairing Multi-Player Games}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {325--339},
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.325},
URN = {urn:nbn:de:0030-drops-53741},
doi = {10.4230/LIPIcs.CONCUR.2015.325},
annote = {Keywords: Nash equilibrium, concurrent games, repair}
}
Document
An Automata-Theoretic Approach to the Verification of Distributed Algorithms
Abstract
We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete.
Cite as
Cyriac Aiswarya, Benedikt Bollig, and Paul Gastin. An Automata-Theoretic Approach to the Verification of Distributed Algorithms. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 340-353, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{aiswarya_et_al:LIPIcs.CONCUR.2015.340,
author = {Aiswarya, Cyriac and Bollig, Benedikt and Gastin, Paul},
title = {{An Automata-Theoretic Approach to the Verification of Distributed Algorithms}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {340--353},
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.340},
URN = {urn:nbn:de:0030-drops-53737},
doi = {10.4230/LIPIcs.CONCUR.2015.340},
annote = {Keywords: distributed algorithms, verification, leader election}
}
Document
Lazy Probabilistic Model Checking without Determinisation
Abstract
The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration.
In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach - both explicit and symbolic versions - in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.
Cite as
Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy Probabilistic Model Checking without Determinisation. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 354-367, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hahn_et_al:LIPIcs.CONCUR.2015.354,
author = {Hahn, Ernst Moritz and Li, Guangyuan and Schewe, Sven and Turrini, Andrea and Zhang, Lijun},
title = {{Lazy Probabilistic Model Checking without Determinisation}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {354--367},
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.354},
URN = {urn:nbn:de:0030-drops-53918},
doi = {10.4230/LIPIcs.CONCUR.2015.354},
annote = {Keywords: Markov decision processes, model checking, PLTL, determinisation}
}
Document
A Modular Approach for Büchi Determinization
Abstract
The problem of Büchi determinization is a fundamental problem with important applications in reactive synthesis, multi-agent systems and probabilistic verification. The first asymptotically optimal Büchi determinization (a.k.a the Safra construction), was published in 1988. While asymptotically optimal, the Safra construction is notorious for its technical complexity and opaqueness in terms of intuition. While some improvements were published since the Safra construction, notably Kähler and Wilke’s construction, understanding the constructions remains a non-trivial task.
In this paper we present a modular approach to Büchi determinization, where the difficulties are addressed one at a time, rather than simultaneously, making the solutions natural and easy to understand. We build on the notion of the skeleton trees of Kähler and Wilke. We first show how to construct a deterministic automaton in the case the skeleton's width is one. Then we show how to construct a deterministic automaton in the case the skeleton's width is k (for any given k). The overall construction is obtained by running in parallel the automata for all widths.
Cite as
Dana Fisman and Yoad Lustig. A Modular Approach for Büchi Determinization. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 368-382, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fisman_et_al:LIPIcs.CONCUR.2015.368,
author = {Fisman, Dana and Lustig, Yoad},
title = {{A Modular Approach for B\"{u}chi Determinization}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {368--382},
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.368},
URN = {urn:nbn:de:0030-drops-53899},
doi = {10.4230/LIPIcs.CONCUR.2015.368},
annote = {Keywords: B\"{u}chi automata, Determinization, Verification, Games, Synthesis}
}
Document
On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference
Abstract
Pushdown systems with transductions (TrPDSs) are an extension of pushdown systems (PDSs) by associating each transition rule with a transduction, which allows to inspect and modify the stack content at each step of a transition rule. It was shown by Uezato and Minamide that TrPDSs can model PDSs with checkpoint and discrete-timed PDSs. Moreover, TrPDSs can be simulated by PDSs and the predecessor configurations pre^*(C) of a regular set C of configurations can be computed by a saturation procedure when the closure of the transductions in TrPDSs is finite. In this work, we comprehensively investigate the reachability problem of finite TrPDSs. We propose a novel saturation procedure to compute pre^*(C) for finite TrPDSs. Also, we introduce a saturation procedure to compute the successor configurations post^*(C) of a regular set C of configurations for finite TrPDSs. From these two saturation procedures, we present two efficient implementation algorithms to compute pre^*(C) and post^*(C). Finally, we show how the presence of transductions enables the modeling of Boolean programs with call-by-reference parameter passing. The TrPDS model has finite closure of transductions which results in model-checking approach for Boolean programs with call-by-reference parameter passing against safety properties.
Cite as
Fu Song, Weikai Miao, Geguang Pu, and Min Zhang. On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 383-397, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{song_et_al:LIPIcs.CONCUR.2015.383,
author = {Song, Fu and Miao, Weikai and Pu, Geguang and Zhang, Min},
title = {{On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {383--397},
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.383},
URN = {urn:nbn:de:0030-drops-53624},
doi = {10.4230/LIPIcs.CONCUR.2015.383},
annote = {Keywords: Verification, Reachability problem, Pushdown system with transductions, Boolean programs with call-by-reference}
}
Document
Characteristic Bisimulation for Higher-Order Session Processes
Abstract
Characterising contextual equivalence is a long-standing issue for higher-order (process) languages. In the setting of a higher-order pi-calculus with sessions, we develop characteristic bisimilarity, a typed bisimilarity which fully characterises contextual equivalence. To our knowledge, ours is the first characterisation of its kind. Using simple values inhabiting (session) types, our approach distinguishes from untyped methods for characterising contextual equivalence in higher-order processes: we show that observing as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes. We demonstrate how characteristic bisimilarity can be used to justify optimisations in session protocols with mobile code communication.
Cite as
Dimitrios Kouzapas, Jorge A. Pérez, and Nobuko Yoshida. Characteristic Bisimulation for Higher-Order Session Processes. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 398-411, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kouzapas_et_al:LIPIcs.CONCUR.2015.398,
author = {Kouzapas, Dimitrios and P\'{e}rez, Jorge A. and Yoshida, Nobuko},
title = {{Characteristic Bisimulation for Higher-Order Session Processes}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {398--411},
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.398},
URN = {urn:nbn:de:0030-drops-53659},
doi = {10.4230/LIPIcs.CONCUR.2015.398},
annote = {Keywords: Behavioural equivalences, session types, higher-order process calculi}
}
Document
Multiparty Session Types as Coherence Proofs
Abstract
We propose a Curry-Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.
Cite as
Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty Session Types as Coherence Proofs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 412-426, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{carbone_et_al:LIPIcs.CONCUR.2015.412,
author = {Carbone, Marco and Montesi, Fabrizio and Sch\"{u}rmann, Carsten and Yoshida, Nobuko},
title = {{Multiparty Session Types as Coherence Proofs}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {412--426},
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.412},
URN = {urn:nbn:de:0030-drops-53661},
doi = {10.4230/LIPIcs.CONCUR.2015.412},
annote = {Keywords: Programming languages, Type systems, Session Types, Linear Logic}
}
Document
On Coinduction and Quantum Lambda Calculi
Abstract
In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear contexts, where programs are used or executed once, is more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence.
Cite as
Yuxin Deng, Yuan Feng, and Ugo Dal Lago. On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 427-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{deng_et_al:LIPIcs.CONCUR.2015.427,
author = {Deng, Yuxin and Feng, Yuan and Dal Lago, Ugo},
title = {{On Coinduction and Quantum Lambda Calculi}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {427--440},
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.427},
URN = {urn:nbn:de:0030-drops-53883},
doi = {10.4230/LIPIcs.CONCUR.2015.427},
annote = {Keywords: Quantum lambda calculi, contextual equivalence, bisimulation}
}
Document
Toward Automatic Verification of Quantum Cryptographic Protocols
Abstract
Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security are obviously guaranteed, with at most an exponentially decreasing gap.
Cite as
Yuan Feng and Mingsheng Ying. Toward Automatic Verification of Quantum Cryptographic Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 441-455, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{feng_et_al:LIPIcs.CONCUR.2015.441,
author = {Feng, Yuan and Ying, Mingsheng},
title = {{Toward Automatic Verification of Quantum Cryptographic Protocols}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {441--455},
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.441},
URN = {urn:nbn:de:0030-drops-53936},
doi = {10.4230/LIPIcs.CONCUR.2015.441},
annote = {Keywords: Quantum cryptographic protocols, Verification, Bisimulation, Security}
}
Document
Unfolding-based Partial Order Reduction
Abstract
Partial order reduction (POR) and net unfoldings are two alternative methods to tackle state-space explosion caused by concurrency. In this paper, we propose the combination of both approaches in an effort to combine their strengths. We first define, for an abstract execution model, unfolding semantics parameterized over an arbitrary independence relation. Based on it, our main contribution is a novel stateless POR algorithm that explores at most one execution per Mazurkiewicz trace, and in general, can explore exponentially fewer, thus achieving a form of super-optimality. Furthermore, our unfolding-based POR copes with non-terminating executions and incorporates state caching. On benchmarks with busy-waits, among others, our experiments show a dramatic reduction in the number of executions when compared to a state-of-the-art DPOR.
Cite as
César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. Unfolding-based Partial Order Reduction. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 456-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{rodriguez_et_al:LIPIcs.CONCUR.2015.456,
author = {Rodr{\'\i}guez, C\'{e}sar and Sousa, Marcelo and Sharma, Subodh and Kroening, Daniel},
title = {{Unfolding-based Partial Order Reduction}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {456--469},
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.456},
URN = {urn:nbn:de:0030-drops-53637},
doi = {10.4230/LIPIcs.CONCUR.2015.456},
annote = {Keywords: Partial order reduction, unfoldings, concurrency, model checking}
}
Document
Verification of Population Protocols
Abstract
Population protocols [Angluin et al., PODC, 2004] are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint.
A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value.
While the predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? We prove that both problems are decidable. Our results also prove decidability of a natural question about home spaces of Petri nets.
Cite as
Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of Population Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 470-482, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{esparza_et_al:LIPIcs.CONCUR.2015.470,
author = {Esparza, Javier and Ganty, Pierre and Leroux, J\'{e}r\^{o}me and Majumdar, Rupak},
title = {{Verification of Population Protocols}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {470--482},
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.470},
URN = {urn:nbn:de:0030-drops-53770},
doi = {10.4230/LIPIcs.CONCUR.2015.470},
annote = {Keywords: Population protocols, Petri nets, parametrized verification}
}
Document
Rely/Guarantee Reasoning for Asynchronous Programs
Abstract
Asynchronous programming has become ubiquitous in smartphone and web application development, as well as in the development of server-side and system applications. Many of the uses of asynchrony can be modeled by extending programming languages with asynchronous procedure calls - procedures not executed immediately, but stored and selected for execution at a later point by a non-deterministic scheduler. Asynchronous calls induce a flow of control that is difficult to reason about, which in turn makes formal verification of asynchronous programs challenging. In response, we take a rely/guarantee approach: Each asynchronous procedure is verified separately with respect to its rely and guarantee predicates; the correctness of the whole program then follows from the natural conditions the rely/guarantee predicates have to satisfy. In this way, the verification of asynchronous programs is modularly decomposed into the more usual verification of sequential programs with synchronous calls. For the sequential program verification we use Hoare-style deductive reasoning, which we demonstrate on several simplified examples. These examples were inspired from programs written in C using the popular Libevent library; they are manually annotated and verified within the state-of-the-art Frama-C platform.
Cite as
Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis. Rely/Guarantee Reasoning for Asynchronous Programs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 483-496, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{gavran_et_al:LIPIcs.CONCUR.2015.483,
author = {Gavran, Ivan and Niksic, Filip and Kanade, Aditya and Majumdar, Rupak and Vafeiadis, Viktor},
title = {{Rely/Guarantee Reasoning for Asynchronous Programs}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {483--496},
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.483},
URN = {urn:nbn:de:0030-drops-53902},
doi = {10.4230/LIPIcs.CONCUR.2015.483},
annote = {Keywords: Asynchronous programs, rely/guarantee reasoning}
}
Document
Partial Order Reduction for Security Protocols
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}
}