ABSTRACT. With the rapid development of feedback control, sensor techniques and computer control, time delay has become an essential feature of cyber-physical systems (CPSs), underlying both the continuous evolution of physical plants and the discrete transition of computer programs, which may well annihilate the stability/safety certificate and control performance of CPSs. In the safety-critical context, automatic verification and synthesis methods addressing time-delay in CPSs should therefore abound. However, surprisingly, they do not, although time-delay has been extensively studied in the literature of mathematics and control theory from a qualitative perspective. In this talk, we will report our recent efforts to tackle these issues, including controller synthesis for time-delayed systems in the setting of discrete time, bounded and unbounded verification of delay differential equations, and discuss remaining challenges and future trends.

ABSTRACT. Qsimulation is a tool for simulating quantum computation on classical computers, which allows a user to write quantum programs in a simple quantum language, draw quantum circuts, and view the results of executing them. Similar to many other quantum simulation tools, the performance of Qsimulation largely depends on its capacity of dealing with matrix operations. In this paper we present Qsimulation V2.0, an optimized quantum simulator that implements a new algorithm for accelerating matrix-vector multiplications. The algorithm is based on matrix decomposition using tensor products and suitable for simulating the execution of quantum circuits. Experimental results show that Qsimulation V2.0 outperforms the open source frameworks Qiskit and ProjectQ.

ABSTRACT. A classic result in formal language theory is the equivalence among aperiodic finite automata, star-free regular expressions, and first-order logic on words. Extending these results to structured subclasses of context-free languages, such as tree languages, did not work as smoothly: there are star-free tree languages that are counting. We argue that investigating the same properties within the family of operator precedence languages (OPLs) by going back to string languages rather than tree languages may lead to equivalences that perfectly match those on regular languages. We define operator precedence expressions; we show that they define exactly the class of OPLs and that, when restricted to the star-free subclass, coincide with first-order definable OPLs and are aperiodic. Since operator precedence languages strictly include other classes of structured languages such as visibly pushdown languages, the same results given in this paper hold as trivial corollary for that family too.

ABSTRACT. We propose a new symbolic trace semantics for register automata (extended finite state machines) which records both the sequence of input symbols that occur during a run as well as the constraints on input parameters that are imposed by this run. Our main result is a generalization of the classical Myhill-Nerode theorem to this symbolic setting. Whereas the Myhill-Nerode theorem refers to a single equivalence relation on words, and constructs a DFA in which states are equivalence classes, our generalization requires the use of three relations to capture the additional structure of register automata. Location equivalence captures that symbolic traces end in the same location, transition equivalence captures that they share the same final transition, and a partial equivalence relation captures that symbolic values v and v' are stored in the same register after symbolic traces w and w', respectively. A symbolic language is defined to be regular if location, transition and register relations exist that satisfy certain conditions, in particular, they all have finite index. We show that the symbolic language associated to a register automaton is regular, and we construct, for each regular symbolic language, a register automaton that accepts this language. Our result provides a foundation for grey-box learning algorithms in settings where the constraints on data parameters can be extracted from code using e.g. tools for symbolic/concolic execution or tainting. We believe that moving to a grey-box setting is essential to overcome the scalability problems of state-of-the-art black-box learning algorithms.

ABSTRACT. We study guarantees for safe communication in systems of systems composed of reactive components that communicate through synchronised execution of common actions. Systems are modelled as (extended) team automata, in which, in principle, any number of component automata can participate in the execution of a communicating action, either as a sender or as a receiver. We extend team automata with synchronisation type specifications, which determine specific synchronisation policies fine-tuned for particular application domains. On the other hand, synchronisation type specifications generate communication requirements for receptiveness and responsiveness. We propose a new (less restrictive) version of requirement satisfaction which allows teams to execute arbitrary intermediate actions before being ready for the required communication, which is important in practice. Then we turn to the composition of systems and show that composition behaves well with respect to synchronisation type specifications. As a central result, we investigate criteria that ensure the preservation of local communication properties when (extended) team automata are composed. This is particularly challenging in the context of weak requirement satisfaction.

ABSTRACT. For a Boolean type of nets \tau, a transition system A is synthesizeable into a \tau-net N if and only if distinct states of A correspond to distinct markings of N, and N prevents a transition firing if there is no related transition in A. The former property is called \tau-state separation property (\tau-SSP) while the latter -- \tau-event/state separation property (\tau-ESSP). A is embeddable into the reachability graph of a \tau-net N if and only if A has the \tau-SSP. This paper presents a complete characterization of the computational complexity of \tau-SSP for all Boolean Petri net types.

ABSTRACT. Software-intensive systems can have thousands of interdependent configuration options across different subsystems. Feature models allow designers to organize the configuration space by describing configuration options using interdependent features: a feature is a name representing some functionality and each software variant is identified by a set of features. Different representations of feature models have been proposed in the literature. In this paper we focus on the propositional representation (which works well in practice) and the extensional representation (which has been recently shown well suited for theoretical investigations). We provide an algebraic and a propositional characterization of feature model operations and relations, and we formalize the connection between the two characterizations as monomorphisms from lattices of propositional feature models to lattices of extensional features models. This formalization shed new light on the correspondence between the extensional and the propositional representations of feature models. It aims to foster the development of a formal framework for supporting practical exploitation of future theoretical developments on feature models and software product lines.

ABSTRACT. Prob-solvable loops are probabilistic programs with polynomial assignments over random variables and parametrised distributions, for which the full automation of moment-based invariant generation is decidable. In this paper we extend Prob-solvable loops with new features essential for encoding Bayesian networks (BNs), which are graphical probabilistic models used in machine learning and AI. We show that various BNs, such as discrete, Gaussian, conditional linear Gaussian and dynamic BNs, can naturally be encoded as Prob-solvable loops. Thanks to these encodings, we automatatically solve several BN related problems, including exact inference, sensitivity analysis, filtering and computing the expected number of rejecting samples in sampling-based procedures. We evaluate our work on a number of BN benchmark, showcasing the full automation of our approach based on Prob-solvable program analysis.

ABSTRACT. Let \tau be a Boolean type of net. The problem occupancy \rho-restricted \tau-synthesis (OR\tau S) is the task to decide for a given transition system A and a natural number \rho whether there is a Boolean Petri net N of type \tau (a \tau-net) whose reachability graph is isomorphic to A and, moreover, every place p of N contains a token in at most \rho reachable markings. In case of a positive decision, N should be constructed. In this paper, we argue that OR\tau S is fixed-parameter-tractable when parameterized by \rho.

ABSTRACT. We study the combinatorial structure of concurrent programs with non-deterministic choice and a fork-join style of coordination. As a first step we establish a link between these concurrent programs and a class of combinatorial structures. Based on this combinatorial interpretation, we develop and experiment algorithms aimed at the statistical exploration of the state-space of programs. The first algorithm is a uniform random sampler of bounded executions, providing a suitable default exploration strategy. The second algorithm is a random sampler of execution prefixes that allows to control the exploration with respect to the uniform distribution. The fundamental characteristic of these algorithms is that they work on the control graph of the programs and not directly on their state-space, thus providing a way to tackle the state explosion problem.