In this talk, I will investigate the expressive power and the algorithmic properties of weighted expressions, which define functions from finite words to integers. First, I will consider a slight extension of an expression formalism, introduced by Chatterjee. et. al. in the context of infinite words (called Mean-Payoff expressions), by which to combine values given by unambiguous (max,+)-automata, using Presburger arithmetic. Important decision problems such as emptiness, universality and comparison are PSpace-Complete for these expressions. I will then investigate the extension of these expressions with Kleene star. This allows to iterate an expression over smaller fragments of the input word, and to combine the results by taking their iterated sum. Unfortunately, the decision problems turn out to be undecidable. So, the goal of this talk is to highlights a still expressive class of expression and sketch is decidability especially by considering a new class of automata: Weighted chop automata.
Data nets are yet another extension of Petri Nets in which the relations between consumed and produced tokens are very restricted. Their subclasses like, Unordered Data Petri Nets (UDPN), from the theory perspective are natural and easy to define. Furthermore, similarly
to Petri Nets they have a lot of structure to explore. During the talk, we will start form defining Data Nets and formulating the state equation, a generalization of one of the simplest and most important equations for Petri Nets.
Next, I will present a sketch of the proof of the correctness of the NP-time algorithm, to solve the equation in case of Unordered Data Petri Nets. Finally, I will mention some novel results for other classes of Data Nets and open problems that we are working on.
The talk will base on a joint work with Patrick Totzke and Jerome Leroux
“Linear Combinations of Unordered Data Vectors” published at LICS-2017
and on unpublished results with Sławomir Lasota.
Reachability analysis is a useful tool for checking whether a cyber-physical system satisfies a given safety property. For instance, one could ask whether an electro-magnetic braking system brings a car to a standstill within a given time frame. In set-based reachability, one takes a given set of initial states (ranges for the position and speed of the car) and computes the image of the set of states as it evolves over time. Even for simple types of systems, this so-called reach set can only be computed approximately, and accuracy comes at an extremely steep cost. A highly scalable way to approximate the reach set is known for the special case of linear dynamics. It is based on template polyhedra, which are polyhedra (sets bounded by linear constraints) with normal vectors from a given finite set. Simple instances of template polyhedra are boxes or octagons. A template instance that tightly bounds the reach set is found by solving a set of optimization problems. The accuracy of the approximation can be improved by adding more normal vectors to the template.
In this talk, we propose an approach that extends this idea from linear to nonlinear dynamics. We linearize the system around a reference trajectory and solve ODEs to obtain templates that bound the reach set. The ODEs are particular in that they involve an optimization problem constrained by the template itself. We show how, similarly to the linear case, the template can be adapted over time to match the dynamics of the system. For both static and dynamic templates, we identify conditions that guarantee convergence. The potential of the approach is discussed on several benchmarks.
In this talk, I will address talk about two projects. The first project deals with the question how we can reason about asynchronous programs. We present a program logic and a corresponding type system that allow us to reason locally about programs with asynchronous concurrency and mutable state; we instantiate this model for OCaml using the Lwt library. The key innovation is to introduce the concept of a “wait permission”, which describes the resources that a given task will yield on termination. An earlier version of this work was published at ECOOP ’15. The second project deals with the question how we can perform a kind of “asynchronous parallelization” optimization, where we are given a (more-or-less) sequential program and rewrite it to make use of asynchronous concurrency. We use a set of program rewriting rules, most notably replacing synchronous I/O operations with asynchronous counterparts in a safe way, and pushing wait statements as far back as possible. As it turns out, proving the soundness of these rewriting rules is surprisingly tricky; I will sketch a reasoning approach that allows us to show refinement, in the the following sense: Let $e$ be a program, and $e’$ the result of rewriting $e$ using the given rules. For every terminating execution of $e’$, there is a corresponding terminating execution of $e$ that ends in an equivalent state.
The central problem addressed in this talk is the following: given the design of a hybrid system, conclude if the system is stable. Hybrid systems are apt to model cyber-physical systems since they capture the mixed discrete-continuous behaviour which appears naturally in cyber-physical systems. Stability is a fundamental property in control system design, which demands that small perturbations in the input to the system lead to small variations in the future behaviour. The classical approach to establishing stability involves finding a particular kind of function, called Lyapunov function. In relation to this method, there is some effort towards automation which consists of a template-based search that uses sum-of-squares solvers. However, the shortcomings with this template-based method are that the choice of a correct template requires designer’s ingenuity and that a template failure does not provide instability reasons or guidance for the choice of the next template.
We propose an alternate algorithmic approach for the stability verification of hybrid systems, which is a counterexample-guided abstraction refinement (CEGAR) framework. The key idea is that given a hybrid system, its stability can be determined by constructing an abstract weighted graph which over-approximates the behaviour of the former one. The relation between the abstraction and the hybrid system is such that if every cycle in the graph has weight below 1, then the hybrid system is stable. In the case that the graph has a cycle with weight greater than 1, this cycle can be evaluated to infer instability of the hybrid system or guide the choice of subsequent templates. This CEGAR approach addresses the shortcomings of the template-based search.
We have implemented the CEGAR algorithm in the tool AVERIST, and we report experimental evaluations on some examples for demonstrating the feasibility of the approach.