2016 - Technical Reports
Number Report Title 2016/1 Effective partial solvers for parity games
Patrick Ah-Fat and Michael Huth, 33pp
2016/2 Simulating Services-Based Systems Hosted in Networks with Dynamic Topology
Petr Novotny and Alexander L. Wolf, 14pp
2016/3 ChairMaker - A Parametric Chair Modelling Program
Kate Reed and Duncan Gillies, 15pp
2016/4 High Volume Ergonomic Simulation of Chairs
Kate Reed and Duncan Gillies, 28pp
2016/5 Interconnection Networks in Session-based Logical Processes
Bernardo Toninho, Nobuko Yoshida, 18pp
2016/6 Modular Termination Verification for Non-blocking Concurrency
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner and Julian Sutherland, 63pp
2016/7 Emulating Web Services-Based Systems Hosted in Ad Hoc Wireless Networks
Petr Novotny and Alexander L. Wolf, pp
2016/8 Polarization Imaging Reflectometry in the Wild
Jeremy Riviere, Ilya Reshetouski, Abhijeet Ghosh, 11pp
2016/9 On the Undecidability of Asynchronous Session Subtyping
Julien Lange and Nobuko Yoshida, 35pp
2016/10 Let It Recover: Multiparty Protocol-Induced Recovery
Rumyana Neykova and Nobuko Yoshida, 14pp
Patrick Ah-Fat and Michael Huth, 33ppReport: 2016/1
Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-time partial solvers can be in principle by studying polynomial-time interactions of partial solvers. Concretely, we propose simple, generic composition patterns for partial solvers that preserve polynomial- time computability. We show that an implementation of this semantic framework manually discovers new partial solvers – including those that merge node sets that have the same but unknown winner – by studying games that composed partial solvers can neither solve nor simplify. We experimentally validate that this data-driven approach to refinement leads to polynomial-time partial solvers that can solve all standard benchmarks of structured games. For one of these polynomial-time partial solvers, we were unable to find even a sole random game that it won’t solve completely, although we generated a few billion random games of varying configurations to that end. However, the work presented here does not yet offer any deeper characterisations of which games are completely solved by such partial solvers.
Petr Novotny and Alexander L. Wolf, 14ppReport: 2016/2
The emerging use of mobile ad hoc networks combined with current trends in the use of service-based systems pose new challenges to accurate simulation of these systems. Current network simulators lack the ability to replicate the complex message exchange behaviour of services, while service simulators do not accurately capture of mobile network properties. In this paper we provide an overview of a framework for simulating both a service behavioural model and a mobile network. The framework is implemented as an extension of the NS-3 network simulator.
Kate Reed and Duncan Gillies, 15ppReport: 2016/3
ChairMaker is a new parametric modelling program that can design 3D chairs. The parameters control physical traits such as back height and seat width. ChairMaker is capable of producing a vast range of semi-realistic 3D models from a set of 33 parameters, with little or no input from human designers. It is intended that these models will be used to explore automated chair design. They also have the potential for use in digital environments such as games, or to be 3D-printed for use in the real world.
Kate Reed and Duncan Gillies, 28ppReport: 2016/4
When designing chairs, ergonomics is a vital component to determine if the chair is suitable for its purpose. To enable the study of automated chair design we require large data sets measuring the suitability of different chair designs, both good and bad, to use with machine learning. We have created a system that designs chairs automatically, but as they exist only as designs and have not been fabricated, physical testing is not possible. To understand what makes a chair comfortable or practical we need to use ergonomic simulations. The simulations presented here can be applied to the automatically designed chairs, and produce pressure maps, along with several other measures of comfort and practicality. The method of simulation is simpler, but much faster than examples in the literature, facilitating the collection of thousands of results.
Bernardo Toninho, Nobuko Yoshida, 18ppReport: 2016/5
In multiparty session types, interconnection networks identify which roles in a session engage in direct communication. If role p is connected to role q, then p exchanges a message with q. In a session-based interpretation of classical linear logic (CLL), this corresponds to the composition, or cut, of dual propositions. This paper shows that well-formed interactions represented in a session-based interpretation of CLL form strictly less expressive interconnection networks than those specified in a multiparty session calculus. To achieve this, we introduce a new compositional synthesis property, dubbed partial multiparty compatibility (PMC), enabling us to build a global type denoting the interactions obtained by iterated composition of well-typed CLL processes. We show that the CLL composition rule induces PMC global types without circular interconnections between three participants. PMC is then used to define a new CLL multicut rule which can form general multiparty interconnections, preserving the deadlock-freedom property of CLL.
Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner and Julian Sutherland, 63ppReport: 2016/6
We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.
Petr Novotny and Alexander L. Wolf, ppReport: 2016/7
The emerging use of ad hoc wireless networks combined with current trends in the use of Web Services-based systems pose new challenges to accurate emulation of these systems. Current network simulators lack the ability to replicate the complex message exchange behavior of services while service simulators do not accurately capture mobile network properties. In this paper, we provide an overview of a generic Web Services framework for emulating both a service behavioral model and an ad hoc wireless network. The framework is implemented as a generic Web Services system in Java EE hosted in the CORE/EMANE emulation environment.
Jeremy Riviere, Ilya Reshetouski, Abhijeet Ghosh, 11ppReport: 2016/8
We present a novel approach for on-site acquisition of surface reflectance for planar, spatially varying, isotropic materials in uncontrolled outdoor environments. Our method exploits the naturally occuring linear polarization of incident illumination: by rotating a linear polarizing filter in front of a camera at 3 different orientations, we measure the linear polarization reflected off the sample and combine this information with multiview analysis and inverse rendering in order to recover per-pixel, high resolution reflectance maps. We exploit polarization both for diffuse/specular separation and surface normals estimation by combining polarization measurements from at least two near orthogonal views close to Brewster angle of incidence. We then use our estimates of surface normals and albedos in an inverse rendering framework to recover specular roughness. To the best of our knowledge, our method is the first to successfully extract a complete set of reflectance parameters with passive capture in completely uncontrolled outdoor environments.
Julien Lange and Nobuko Yoshida, 35ppReport: 2016/9
Asynchronous session subtyping has been studied extensively in [8,9,28–31] and applied in [23,32,33,35]. An open question was whether this subtyping relation is decidable. This paper settles the question in the negative. To prove this result, we first introduce a new sub-class of two-party communicating finite-state machines (CFSMs), called asynchronous duplex (ADs), which we show to be Turing complete. Secondly, we give a compatibility relation over CFSMs, which is sound and complete wrt. safety for ADs, and is equivalent to the asynchronous subtyping. Then we show that checking whether two CFSMs are in the relation reduces to the halting problem for Turing machines. In addition, we show the compatibility relation to be decidable for three sub-classes of ADs.
Rumyana Neykova and Nobuko Yoshida, 14ppReport: 2016/10
Fault-tolerant communication systems rely on recovery strategies which are often error-prone (e.g. a programmer manually specifies recovery strategies) or inefficient (e.g. the whole system is restarted from the beginning). This paper proposes a static analysis based on multiparty session types that can efficiently compute a safe global state from which a system of interacting processes should be recovered. We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. We formalise our recovery algorithm and prove its safety. A recovered communication system is free from deadlocks, orphan messages and reception errors. Our recovery algorithm incurs less communication cost (only affected processes are notified) and overall execution time (only required states are repeated). On top of our analysis, we design and implement a runtime framework in Erlang where failed processes and their dependencies are soundly restarted from a computed safe state. We evaluate our recovery framework on message-passing benchmarks and a use case for crawling webpages. The experimental results indicate our framework outperforms a built-in static recovery strategy in Erlang when a part of the protocol can be safely recovered.