Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering


Computational Engines

Theme Leaders: Paulo Tabuada (UCLA) and Moshe Vardi (Rice)

Contributors: Alur (Penn), Kavraki (Rice), Kress-Gazit (Cornell), Lafortune (Michigan), Partharathy (UIUC), Sesia (Berkeley), Solar-Lezama (MIT), Tripakis (Berkeley)

The research theme of Computational Engines explores common algorithmic foundations for formalizing and solving different versions of the synthesis problem. Algorithmic foundations for synthesis on multiple fronts is studied. Representative fronts include probabilistic systems, concurrent systems, linear control systems, hybrid systems, and quantitative analysis. A recently launched collaborative effort aims at defining the problem of syntax-guided synthesis modulo theories in a rigorous and general way so that the community can share benchmarks and algorithmic solutions.

Reactive Synthesis vs. Supervisory Control: Bridging the Gap

This work aims to establish a formal connection between synthesis problems that have been considered, largely separately, in the two research communities of control engineering and formal methods. By making this connection mathematically precise, we aim to bridge the gap between two research areas that tackle similar synthesis problems, but from different angles, and by emphasizing different, and often complementary, aspects. Such a formal bridge will be a source of inspiration for new lines of investigation that will leverage the power of the synthesis techniques that have been developed in these two areas.

Synthesis for Hybrid Systems with Maximal Satisfaction Guarantees

We developed a novel theoretical and computational framework for control synthesis for hybrid systems with general nonlinear continuous dynamics from specifications given as a conjunction of a syntactically co-safe and a syntactically safe linear temporal logic (LTL) formulas. If the specification found unsatisfiable by the hybrid system, the framework computes controls that lead to a user-desired partial satisfaction of the liveness segment of the specification without violating the safety requirements. The approach is based on a synergistic combination of planning layers developed in a prior work. Experiments on a hybrid robotic system with nonlinear dynamics demonstrate that the synthesis framework produces satisfactory behaviors when the LTL specification is not fully achievable.

Synthesis for Nondeterministic Hybrid Systems

We have initiated an effort to examine the problem of synthesis for nondeterministic hybrid systems with complex continuous dynamics and nondeterministic discrete switching between them from a temporal logic specification. Our intention is to employ sampling-based techniques that can deal with nonlinear continuous dynamics and combine it with game-theoretic approaches to handle discrete nondeterminism. The goal of this project is to compute winning strategies for the system to achieve the specification by viewing nondeterminism as an adversary. We will access the framework on a second-order car-like robot in an environment that includes several unknown terrains where moving over each terrain could affect the motion of the robot. In the long run, we are interested in including such systems in synthesis frameworks, a task that is not possible with available machinery.

Distribution-Aware Sampling Techniques

We designed novel algorithms and developed reference implementations for weighted model counting and distributionaware sampling of satisfying assignments for a SAT formula. The project was motivated by important applications in synthesis tools. In particular, a distribution-aware sampling used in the underlying solvers for sketch-based synthesis provided guarantees on the convergence to an optimal solution. On the other hand, weighted model counting forms the backbone of computational engines for automatic problem generation in context of MOOCs.

Synthesis with Identifiers

We consider the synthesis of reactive systems from temporal specifications with identifiers, which can parametrize the input and output. We give a new specification formalism for this problem, prove that the synthesis problem is undecidable, and give a sound algorithm based on computing a pattern-based abstraction of the original synthesis game. Results are demonstrated on the Robot Waiter challenge problem formalized in Year 1 of the ExCAPE project. This is one of the first results that extends the theory of synthesis from temporal logic to a richer class of specifications and to synthesis of infinite-state systems.

Synthesis from Component Libraries

We have started an investigation into the problem of synthesis from component libraries. Our goal is to construct an interface abstraction through which the library components can interact. Our motivation is that by using interfaces, every component can be considered as a black-box, and thus a system can be synthesized when only the specification of every component described by an LTL formula is available to the designer. Moreover, interfaces allow the use of hierarchies of compositions which does not exist in the current state-of-the-art.

Component-based Reactive Synthesis for Probabilistic Systems

Synthesis from components is the automated construction of a composite system from a library of reusable components such that the system satisfies the given specification. This is in contrast to classical synthesis, where systems are always constructed from scratch. In the control-flow model of composition, exactly one component is in control at a given time and control is switched to another when the component reaches an exit state. The composition can then be described implicitly by a transducer, called a composer, which statically determines how the system transitions between components. Recently, it was shown that control-flow synthesis of deterministic composers from libraries of probabilistic components is decidable. In this work, we considered the more general case of probabilistic composers. We showed that probabilistic composers are more expressive than deterministic composers, and that the synthesis problem still remains decidable. In the near future, we will pursue how these theoretical results can help in improving the scalability of reactive synthesis for the robotics application domain

Learning Omega Regular Languages

A major critique of reactive synthesis, the problem of synthesizing a reactive system from a given temporal logic formula, is that it shifts the problem of implementing a system that adheres to the specification in mind to formulating a temporal logic formula that expresses it. A potential customer of a computerized system may find it hard to specify his requirements by means of a temporal logic formula. Instead, he might find it easier to provide good and bad examples of ongoing behaviors (or computations) of the required system, or classify a given computation as good or bad. This is a classical scenario for interactive learning of an unknown language using membership and equivalence queries.

Regular omega languages are the main means to model reactive systems. Learning omega regular languages using membership and equivalence queries thus provides a mechanism for synthesizing an implementation of a reactive system. In this work we address the problem of learning regular omega languages, which was considered open for many years.

Controller Synthesis for Linear Control Systems and Safe Specifications

We developed a novel algorithm to synthesize controllers enforcing linear temporal logic specifications on discrete-time linear control systems. The central step within this approach is the computation of the maximal controlled invariant set contained in a possibly non-convex safe set. Although it is known how to compute approximations of maximal controlled invariant sets, its exact computation remains an open problem. We provide an algorithm which computes a controlled invariant set that is guaranteed to be an under-approximation of the maximal controlled invariant set.

Optimal Performance for Continuous-time Controllers

Recently, formal methods have been used to transform high-level robot tasks into correct-by-construction controllers. While correctness is guaranteed, these inherently discrete methods can often lead to behaviors that are not optimal in the continuous sense, i.e. they induce robot paths that are significantly suboptimal. This work proposes an algorithm for dynamically reordering the robot goals and connecting them with the shortest path based on the given continuous metric. The generated robot trajectories are close-to-optimal while satisfying the original task specification in a dynamic environment. This method is implemented and simulation results are shown. The results are being integrated in the tool LTLMoP to be applied to the Robotics challenge problem.

Synthesis of Controllers for Linear System

In this work, we present and analyze a novel algorithm to synthesize controllers enforcing linear temporal logic specifications on discrete-time linear systems. The central step within this approach is the computation of the maximal controlled invariant set contained in a possibly non-convex safe set. Although it is known how to compute approximations of maximal controlled invariant sets, its exact computation remains an open problem. We provide an algorithm which computes a controlled invariant set that is guaranteed to be an under-approximation of the maximal controlled invariant set. Moreover, we guarantee that our approximation is at least as good as any invariant set whose distance to the boundary of the safe set is lower bounded. The proposed algorithm is founded on the notion of sets adapted to the dynamics and binary decision diagrams. Contrary to most controller synthesis schemes enforcing temporal logic specifications on continuous systems, we do not compute a discrete abstraction of the continuous dynamics. Instead, we abstract only the part of the continuous dynamics that is relevant for the computation of the maximal controlled invariant set.

Synthesis of Robust Control Software

We developed a novel algorithm to synthesize controllers enforcing linear temporal logic specifications on discrete-time linear control systems. The central step within this approach is the computation of the maximal controlled invariant set contained in a possibly non-convex safe set. Although it is known how to compute approximations of maximal controlled invariant sets, its exact computation remains an open problem. We provide an algorithm which computes a controlled invariant set that is guaranteed to be an under-approximation of the maximal controlled invariant set.

Resilience to Intermittent Assumption Violations in Reactive Synthesis

This project considers synthesis of reactive systems that are robust against intermittent violations of their environment assumptions. Such assumptions are needed to allow many systems that work in a larger context to fulfill their tasks. Yet, due to glitches in hardware or exceptional operating conditions, these assumptions do not always hold in the field. Building on generalized reactivity(1) synthesis, a synthesis approach that is well-known to be scalable enough for many practical applications, we show how, starting from a specification that is supported by this synthesis approach, we can modify it in order to use a standard generalized reactivity(1) synthesis procedure to find error-resilient systems. As an added benefit, this approach allows exploring the possible trade-offs in error resilience that a system designer has to make, and to give the designer a list of all Pareto-optimal implementations.

Synthesis of Insertion Functions for Enforcement of Opacity Security Properties

We have investigated a new application domain for reactive synthesis techniques, namely, that of enforcement of security properties in networked systems. Specifically, we have considered the notion of opacity, which captures the ability, or lack thereof, of an intruder to infer a “secret” about a given system, based on its knowledge of the system structure and its observation of the system behavior. In cases where the desired opacity property does not hold, we have developed a novel synthesis methodology for the construction of a suitable interface, in the form of an insertion function, that provably enforces opacity by insertions of additional, fictitious, observable events. Our synthesis methodology is based on the construction of a finite structure that embeds all valid insertion functions. Game-theoretic results on weighted graphs can then be leveraged to synthesize optimal insertion functions when costs are assigned to the inserted events.We have shown how this methodology can be used to enforce privacy of the location of a user of location-based services.

Synthesizing Invariants for Program Verification

When building reliable applications, current techniques for program verification require the programmer to annotate the program with inductive invariants to aid verification. Providing these annotations is one of the biggest challenges that we face in making such techniques useful for programmers. This project aims to aid the programmer by synthesizing these annotations automatically. The focus is on devloping predicate synthesis algorithms using learning. Intuitively, the actual constraints are hidden from the learner, and the learner synthesizes predicates based only on concrete examples with their classification as true/false. Machine learning techniques, which are often very scalable, can then be utilized to build classifiers, which then can be interpreted as logical predicates.

Synthesizing Provably Correct Data-Structure Manipulations

The aim of this project is a marriage of two techniques both developed by ExCAPE researchers: the natural proofs technique from program verification, and the sketching technique from program synthesis. While natural proofs encodes a set of powerful proof tactics into automatically generated ghost code, it allows to use Sketch to synthesize provably correct code snippets from scratch. We currently focus on data-structure manipulations and specs written in the Dryad logic. Technically, we are encoding a symbolic interpreter for Dryad into Sketch, so that Sketch can synthesize code snippets that meet given Dryad specs. Ongoing case studies include basic list/tree manipulations.

Syntax-Guided Synthesis

The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementation.

In this collaborative effort we have defined a logic-based core computational problem so that different algorithmic strategies can be compared in an experimentally rigorous manner and computational advances can be easily shared across tools (such as Sketch and Transit). Based on this definition, we have organized a solvers competition SyGuS-COMP held at FLoC 2014.

Regular String Transformations

Theory of regular languages (of strings, infinite strings, and trees) has proved to be an excellent foundation for qualitative verification and synthesis of finite-state systems. The goal of this research thread is to develop a similarly robust foundation for quantitative analysis and synthesis. We propose a deterministic model for associating costs with strings that is parameterized by operations of interest (such as addition, scaling, and min), a notion of regularity that provides a yardstick to measure expressiveness, and study decision problems and theoretical properties of resulting classes of cost functions. Our definition of regularity relies on the theory of string-to-tree transducers, and allows associating costs with events that are conditional upon regular properties of future events. Our model of cost register automata allows computation of regular functions using multiple "write-only" registers whose values can be combined using the allowed set of operations.

Synthesis of State-Observers Resilient to Sensor Attacks

Motivated by the increasing number of reported attacks on cyber-physical systems (CPS), we are investigating the detection and mitigation of sensor attacks on CPS described by linear dynamics. In particular, our goal is to automatically synthesize algorithms that are able to isolate the sensors that have been compromised by an adversarial attack (detection) while being able to correctly estimate the state of the physical system (mitigation). Our approach combines Satisfiability Modulo Theory (SMT) solvers, convex optimization, and control theory to synthesize state estimators resilient to sensor attacks.

Further reading

Click one of the above items for more info or visit the publications page for papers under the computational engines theme.

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996