2013 - Technical Reports
Number Report Title 2013/1 Fatal Attractors in Parity Games
Michael Huth, Jim Huan-Pu Kuo and Nir Piterman, 31pp
2013/2 An Observationally Complete Program Logic for Imperative Higher-Order Functions
Kohei Honda, Nobuko Yoshida and Martin Berger, 80pp
2013/3 Monitoring Networks through Multiparty Session Types
Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida, 28pp
2013/4 Globally Governed Session Semantics
Dimitrios Kouzapas and Nobuko Yoshida, 32pp
2013/5 Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types
Pierre-Malo DeniÂ´elou and Nobuko Yoshida, 22pp
2013/6 Policy-Based Access Control from Numerical Evidence
Jason Crampton, Michael Huth and Charles Morisset, 21pp
2013/7 PEALT: A Reasoning Tool for Numerical Aggregation of Trust Evidence
Jason Crampton, Michael Huth and Charles Morisset, 14pp
2013/8 A fluid model for closed queueing networks with PS stations
Juan F. Perez and Giuliano Casale, 5pp
2013/9 Group Synthesis for Alternating-Time Temporal Logic
A. V. Jones, M. Knapik, A. Lomuscio, and W. Penczek, 16pp
Michael Huth, Jim Huan-Pu Kuo and Nir Piterman, 31ppReport: 2013/1
We study a new form of attractor in parity games and use it to define solvers that run in PTIME and are partial in that they do not solve all games completely. Technically, for color c this new attractor determines whether player c%2 can reach a set of nodes X of color c whilst avoiding any nodes of color less than c. Such an attractor is fatal if player c%2 can attract all nodes in X back to X in this manner. Our partial solvers detect fixed-points of nodes based on fatal attractors and correctly classify such nodes as won by player c%2.
Experimental results show that our partial solvers completely solve benchmarks that were constructed to challenge existing full solvers. Our partial solvers also have encouraging run times. For one partial solver we prove that its runtime is cubic in the number of nodes, that its output game is independent of the order in which attractors are computed, and that it solves all Buchi games.
Kohei Honda, Nobuko Yoshida and Martin Berger, 80ppReport: 2013/2
We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A systematic use of names and operations on them allows precise and general description of complex higher-order imperative behaviour. The proof rules of the logic exactly follow the syntax of the language and can cleanly embed, justify and extend the standard proof rules for total correctness of Hoare logic. The logic offers a foundation for general treatment of aliasing and local state on its basis, with minimal extensions. After establishing soundness, we prove that valid assertions for programs completely characterise their behaviour up to observational congruence, which is proved using a variant of finite canonical forms. The use of the logic is illustrated through reasoning examples which are hard to assert and infer using existing program logics.
Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida, 28ppReport: 2013/3
In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognized, however the existing frameworks, relying on centralised verifcation or restricted specifcation methods, have limited applicability. This paper proposes a new theory of monitored Π calculus with dynamic usageof multiparty session types (MPST), covering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i.e. equating networks covering the same services to a user. We illustrate our static-dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity.
Dimitrios Kouzapas and Nobuko Yoshida, 32ppReport: 2013/4
This paper proposes a new bisimulation theory based on multiparty session types where a choreography specification governs the behaviour of session typed processes and their observer. The bisimulation is defined with the observer cooperating with the observed process in order to form complete global session scenarios and usable for proving correctness of optimisations for globally coordinating threads and processes. The induced bisimulation is strictly more fine-grained than the standard session bisimulation. The difference between the governed and standard bisimulations only appears when more than two interleaved multiparty sessions exist. This distinct feature enables to reason real scenarios in the large-scale distributed system where multiple choreographic sessions need to be interleaved. The compositionality of the governed bisimilarity is proved through the soundness and completeness with respect to the governed reduction-based congruence. Finally its usage is demonstrated by a thread transformation governed under multiple sessions in a real usecase in the large-scale cyberinfrustracture.
Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session TypesPierre-Malo DeniÂ´elou and Nobuko Yoshida, 22ppReport: 2013/5
Multiparty session types are a type system that can ensure the safety and liveness of distributed peers via the global specification of their interactions. To construct a global specification from a set of distributed uncontrolled behaviours, this paper explores the problem of fully characterising multiparty session types in terms of communicating automata. We equip global and local session types with labelled transition systems (LTSs) that faithfully represent asynchronous communications through unbounded buffered channels. Using the equivalence between the two LTSs, we identify a class of communicating automata that exactly correspond to the projected local types. We exhibit an algorithm to synthesise a global type from a collection of communicating automata. The key property of our findings is the notion of multiparty compatibility which non-trivially extends the duality condition for binary session types.
Jason Crampton, Michael Huth and Charles Morisset, 21ppReport: 2013/6
Increasingly, access to resources needs to be regulated or informed by considerations such as risk, cost, and reputation. We therefore propose a framework for policy languages, based on semi-rings, that aggregate quantitative evidence to support decision-making in access-control systems. As aggregation operators "addition", "worst case", and "best case" over non-negative reals are both relevant in practice and amenable to analysis, we study an instance, Peal, of our framework in that setting. Peal is a stand-alone policy language but can also be integrated with existing policy languages.
Peal policies can be synthesized logical formulae that no longer make reference to quantities but capture all policy behavior. Satisfiability checking of such formulae can be used to validate and analyze policies in this new evidence-based approach. We discuss a number of applications, including vacuity, redundancy, change-impact and safety analysis. The synthesis algorithm requires a form of subset enumeration, for which we develop bespoke algorithms and demonstrate experimentally that our algorithms work better than generic state exploration methods. We also sketch how our approach extends from non-negative reals to other semi-rings and even to rings such as the real numbers.
Jason Crampton, Michael Huth and Charles Morisset, 14ppReport: 2013/7
We present a tool that supports the understanding and validation of mechanisms that numerically aggregate trust evidence which may stem from heterogenous sources such as geographical information, reputation, and threat levels. The tool is based on a policy composition language Peal and can declare Peal expressions and intended analyses of such expressions as input. The analyses include vacuity checking, sensitivity analysis of thresholds, and policy refinement. We develop and implement two methods for generating verification conditions for analyses, using the SMT solver Z3 as backend. One method is explicit and space intense, the other one is symbolic and so linear in the analysis expressions. We experimentally investigate this space-time tradeo by observing the Z3 code generation and its running time on randomly generated analyses and on a non-random benchmark modeling majority voting. Our fndings suggest both methods have complementary value and may scale up suficiently for the analysis of most realistic case studies.
Juan F. Perez and Giuliano Casale, 5ppReport: 2013/8
This technical report introduces a closed multi-class queueing network (QN) model with class-switching, where the service rates are defined to represent multi-processor stations with a processor-sharing (PS) allocation policy. These transition rates are also able to consider traditional delay nodes, and therefore a QN model with these transition rates is well-suited for multi-threaded software applications. In this report, we define the QN model and use the results to show that the transient sample paths of the QN model converge to the solution of a system of ordinary differential equations (ODEs). As the sizeof the ODE system grows linearly with the number of stations and job classes in the QN model, solving the ODE system becomes a scalable alternative to Markov chain representations.
A. V. Jones, M. Knapik, A. Lomuscio, and W. Penczek, 16ppReport: 2013/9
We present an extension of Alternating-time Temporal Logic ATL, called ATLP (Parametric ATL), where parameters are allowed in place of concrete groups of agents. We devise a procedure to find all instantiations for the parameters in a given formula ø of ATLP so that ø oslash; is true in a given model. We propose a formalisation of the problem and symbolic algorithms for its solution. We discuss an experimental implementation of the approach on top of the open-source model checker MCMAS and demonstrate the benefits of the technique through experimental results.