1,721,046 research outputs found
Synthesizing nonanomalous event-based controllers for liveness goals
Full text linkWe present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behaviour models. Our approach works for an expressive subset of liveness properties, distinguishes between controlled and monitored actions, and differentiates system goals from environment assumptions. We show that assumptions must be modelled carefully in order to avoid synthesising anomalous behaviour models. We characterise non-anomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline.Fil: D'ippolito, Nicolás Roque. Imperial College London; Reino Unido. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Braberman, Victor Adrian. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Piterman, Nir. University of Leicester; Reino UnidoFil: Uchitel, Sebastian. Imperial College London; Reino Unido. Universidad de Buenos Aires; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
XSpeed: Accelerating Reachability Analysis on Multi-core Processors
No full textWe present XSpeed a parallel state-space exploration algorithm for continuous systems with linear dynamics and nondeterministic inputs. The motivation of having parallel algorithms is to exploit the computational power of multi-core processors to speed-up performance. The parallelization is achieved on two fronts. First, we propose a parallel implementation of the support function algorithm by sampling functions in parallel. Second, we propose a parallel state-space exploration by slicing the time horizon and computing the reachable states in the time slices in parallel. The second method can be however applied only to a class of linear systems with invertible dynamics and fixed input. A GP-GPU implementation is also presented following a lazy evaluation strategy on support functions. The parallel algorithms are implemented in the tool XSpeed. We evaluated the performance on two benchmarks including an 28 dimension Helicopter model. Comparison with the sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario), the state of the art tool for reachability analysis of linear hybrid systems. Experiments illustrate that our parallel algorithm with time slicing not only speeds-up performance but also improves precision
Resource-Parameterized Timing Analysis of Real-Time Systems
No full textCyber-Physical Systems (CPS) are subject to platform-given resource constraints upon such resources as CPU, memory, and bus, in executing their functionalities. This causes the behavior of a verified application to deviate from its intended timing behavior when the application is integrated on a specic platform. For the same reason, a configuration of platforms cannot be independent from applications in most cases. This paper proposes a new analysis framework of real-time systems where an application and a platform can be analyzed in a fully independent way such that not only the application but also the platform once verfiied can be exploited by various applications. The dependent behaviors of application and platform are also analyzed by exploiting their individual models transformed from their independent models. To the end, we provide a highly configurable platform model that can be parameterized by various resource congurations. For analysis of application and platform models, we use two model checking techniques: symbolic and statistical model checking techniques of Uppaal. Our framework is demonstrated by a case study where a turn indicator system is analyzed with respect to various platform resource constraints
Coverage-Driven Verification:An Approach to Verify Code for Robots that Directly Interact with Humans
Full text linkCollaborative robots could transform several industries, such as manufacturing and healthcare, but they present a significant challenge to verification. The complex nature of their working environment necessitates testing in realistic detail under a broad range of circumstances. We propose the use of Coverage-Driven Verification (CDV) to meet this challenge. By automating the simulation-based testing process as far as possible, CDV provides an efficient route to coverage closure. We discuss the need, practical considerations, and potential benefits of transferring this approach from microelectronic design verification to the field of human-robot interaction. We demonstrate the validity and feasibility of the proposed approach by constructing a custom CDV testbench and applying it to the verification of an object handover task
Synthesis of Event-Based Controllers for Software Engineering
Full text linkBehavioural modelling has been widely used to aid in the design of concurrent
systems. Behaviour models have shown to be useful to uncover design
errors in early stages of the development process. However, building correct
behaviour models is costly and requires significant experience. Controller
synthesis offers a way to build models that are correct by construction. Existing
software engineering techniques for synthesising controllers have various
limitations. Such limitations can be seen as restrictions in the expressiveness
of the controller goals and environment model, or in the relation between
the controllable and monitored actions. The main aim of this thesis is the
development of novel techniques overcoming known limitations of previous
approaches and methodological guidelines for synthesising useful controllers.
This thesis establishes the framework for controller synthesis techniques that
support event-based models, expressive goal specifications, distinguish controllable
from monitored actions and guarantee achievement of the desired
goals. Together with these techniques, methodological guidelines are proposed
to help in building more accurate descriptions of the environment and
more effective controllers.
In addition, this thesis presents a tool that implements the proposed techniques.
Evaluation of the techniques has been conducted using the tool
to model known case studies from the literature, showing that by allowing
more expressive controller goals and environment models, and explicitly distinguishing
controllable and monitored actions such case studies can be more
accurately modelled and solutions guaranteeing satisfaction of the goals can
be achieved
Parity games : descriptive complexity and algorithms for new solvers
Full text linkParity games are 2-person, 0-sum, graph-based, and determined games
that form an important foundational concept in formal methods (see e.g.,
[Zie98]), and their exact computational complexity has been an open problem
for over twenty years now.
In this thesis, we study algorithms that solve parity games in that they
determine which nodes are won by which player, and where such decisions
are supported with winning strategies. We modify and so improve a known
algorithm but also propose new algorithmic approaches to solving parity
games and to understanding their descriptive complexity.
For all of our contributions, we write our own custom frameworks, in the
Scala programming language, to perform tailored experiments and empirical
studies to demonstrate and support our theoretical findings.
First, we improve on one of the solver algorithms, based on small progress
measures [Jur00], by use of concurrency. We show that, for many parity
games, it is possible to deliver extra performance using this technique in a
multi-core environment.
Second, we design algorithms to reduce the computational complexity
of parity games, and create implementations to observe and evaluate the
behaviours of these reductions in our experimental settings. The measure
Rabin index, arising from the design of the said algorithm, is shown to be a
new descriptive complexity for parity games.
Finally, we define a new family of attractors and derive new parity game solvers from them. Although these new solvers are “partial”, in that they
do not solve all parity games completely, our experiments show that they do
solve a set of benchmark games (i.e., games with known structures) designed
to stress test solvers from PGSolver toolkit [FL10] completely, and some of
these partial solvers deliver favourable performance against a known high
performance solver in many circumstances
Model-checking iterated games
No full textWe propose a logic for the definition of the collaborative power of groups of agents to enforce different temporal objectives. The resulting temporal cooperation logic (TCL) extends ATL by allowing for successive definition of strategies for agents and agencies. Different to previous logics with similar aims, our extension cuts a fine line between extending the power and maintaining a low complexity: model-checking TCL sentences is EXPTIME complete in the logic, and fixed parameter tractable for specifications of bounded size. This advancement over non-elementary logics is bought by disallowing a too close entanglement between cooperation and competition. We show how allowing such an entanglement immediately leads to a non-elementary complexity. We have implemented a model-checker for the logic and shown the feasibility of model-checking on a few benchmarks. © 2013 Springer-Verlag
Tools and Algorithms for the Construction and Analysis of Systems − 19th International Conference‚ TACAS 2013‚ Held as Part of the European Joint Conferences on Theory and Practice of Software‚ ETAPS 2013‚ Rome‚ Italy‚ March 16−24‚ 2013. Proceedings
No full textFrom Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata
No full textDeterminisation and complementation are foundational notions in computer science. When considering finite automata on finite words nondeterminisation and complementation are one and the same. Given a nondeterministic finite automaton there exists an exponential construction that gives a deterministic automaton for the same language. Inverting the set of accepting states gives us the automaton for the complement language. In the theory of automata on infinite words determinisation and complementation are much more involved. Safra provides determinisation constructions for B\"uchi and for Streett automata that result in deterministic Rabin automata. The construction starts with an automaton with states (and index for the Streett case) and results in a Rabin automaton with states ( states and index for the Streett case). Here, we reconsider Safra's determinisation constructions. We show how to construct automata with less states, smaller index, and most importantly, parity acceptance condition. Specifically, starting from a nondeterministic B\"uchi automaton with states our construction yields an automaton with states (instead of ), index (instead of ), and a parity automaton (instead of Rabin). Starting from a nondeterministic Streett automaton with states and index our construction yields an automaton with states (instead of ), index (instead of ), and a parity automaton (instead of Rabin). For every practical application, the fact that our automaton is parity saves an additional multiplier of in the case of B\"uchi and in the case of Streett.MT
- …
