Narrow Results

Live sequence charts (LSCs) have been defined recently as an extension of message sequence charts (MSCs; or their UML variant, sequence charts (MSCs; or their UML variant, sequence diagrams) for rich inter-object specification. One of the main additions is the notion of universal charts and hot, mandatory behavior, which, among other things, enables one to specify forbidden scenarios. LSCs are thus essentially as expressive as statecharts. This paper deals with synthesis, which is the problem of deciding, given an LSC specification, if there exists a satisfying object system and, if so, to synthesize one automatically. The synthesis problem is crucial in the development of complex systems, since sequence diagrams serve as the manifestation of use cases — whether used formally or informally — and if synthesizable they could lead directly to implementation. Synthesis is considerably harder for LSCs than for MSCs, and we tackle it by defining consistency, showing that an entire LSC specification is consistent iff it is satisfiable by a state-based object system, and them synthesizing a satisfying system as a collection of finite state machines or statecharts.

We propose a sound and complete compositional proof rule for distributed synthesis. Applying our proof rule only requires the manual strengthening of the specification into a conjunction of formulas that can be guaranteed by individual black-box processes. All premises of the proof rule can be checked automatically.

For this purpose, we give an automata-theoretic synthesis algorithm for single processes in distributed architectures. The behavior of the local environment of a process is unknown in the process of synthesis and cannot be assumed to be maximal. We therefore consider reactive environments that have the power to disable some of their own actions, and provide methods for synthesis (and realizability checking) in this setting. We establish upper bounds for CTL (2EXPTIME) and CTL* (3EXPTIME) synthesis with incomplete information, matching the known lower bounds for these problems, and provide matching upper and lower bounds for μ-calculus synthesis (2EXPTIME) with complete or incomplete information. Synthesis in reactive environments is harder than synthesis in maximal environments, where CTL, CTL* and μ-calculus synthesis are EXPTIME, 2EXPTIME and EXPTIME complete, respectively.

We investigate how two agents can communicate through a noisy medium modeled as a finite non deterministic transducer. The sender and the receiver are also described by finite transducers which can respectively encode and decode binary messages. When the communication is reliable, we call the encoder/decoder pair a channel.

We study the channel synthesis problem which, given a transducer, asks whether or not such sender and receiver exist and builds them if the answer is positive. To that effect we introduce the structural notion of encoding state in a transducer which is a necessary condition for the existence of a channel. It is not, however, a sufficient condition. In fact, we prove that the problem is undecidable. Nonetheless, we obtain a synthesis procedure when the transducer is functional. We discuss these results in relation to security properties.

The synthesis problem asks to automatically generate, if it exists, an algorithm from a specification of correct input-output pairs. In this paper, we consider the synthesis of computable functions of infinite words, for a classical Turing computability notion over infinite inputs. We consider specifications which are rational relations of infinite words, i.e., specifications defined by non-deterministic parity transducers. We prove that the synthesis problem of computable functions from rational specifications is undecidable. We provide an incomplete but sound reduction to some parity game, such that if Eve wins the game, then the rational specification is realizable by a computable function. We prove that this function is even computable by a deterministic two-way transducer.

We provide a sufficient condition under which the latter game reduction is complete. This entails the decidability of the synthesis problem of computable functions, which we proved to be ExpTime-complete, for a large subclass of rational specifications, namely deterministic rational specifications. This subclass contains the class of automatic relations over infinite words, a yardstick in reactive synthesis.

This paper addresses the issue of automatic service composition. We first develop a framework in which the exported behavior of a service is described in terms of a so-called execution tree, that is an abstraction for its possible executions. We then study the case in which such exported behavior (i.e. the execution tree of the service) can be represented by a finite state machine (i.e. finite state transition system). In this specific setting, we devise sound, complete and terminating techniques both to check for the existence of a composition, and to return a composition, if one exists. We also analyze the computational complexity of the proposed algorithms. Finally, we present an open source prototype tool, called (E-Service Composer), that implements our composition technique. To the best of our knowledge, our work is the first attempt to provide a provably correct technique for the automatic synthesis of service composition, in a framework where the behavior of services is explicitly specified.

There are several motives for creating process models ranging from technical scenarios in workflow automation to business scenarios in which management decisions are taken. As a consequence, companies typically have different process models for the same process, which differ in terms of granularity. In this context, business process model abstraction serves as a technique that takes a process model as an input and derives a high-level model with coarse-grained activities and the corresponding control flow between them. In this way, business process model abstraction reduces the number of models capturing the same business process on different abstraction levels. In this article, we provide a solution to the problem of deriving the control flow of an abstract process model for the case that an arbitrary grouping of activities is permitted. To this end, we use behavioral profiles and prove that the soundness of the synthesized process model requires a notion of well-structuredness of the abstract model behavioral profile. Furthermore, we demonstrate that the activities can be grouped according to the data flow of the model in a meaningful way, and that this grouping does not directly coincides with a structural decomposition of the process, which is generally assumed by other abstraction approaches. This finding emphasizes the need for handling arbitrary activity groupings in business process model abstraction.