Abstract Realizability is an important requirement for reactive system specifications. A reactive system interacts with an environment and responds to input events. Realizability ensures the reactive system behaves as specified, no matter how its environment provides input. Typically, reactive system specifications are given using linear temporal logic (LTL), and they can be tested to ascertain whether the specification is realizable. However, the LTL specification realizability problem is 2EXPTIME-complete, which hinders its application to large-scale systems. In this article, we present a modularization method to mitigate this computational challenge.

Linear temporal logic (LTL) synthesis is a formal method for automatically composing a reactive system that realizes a given behavioral specification described in LTL if the specification is realizable. Even if the whole specification is unrealizable, it is preferable to synthesize a best-effort reactive system. That is, a system that maximally realizes its partial specifications. Therefore, we categorized specifications into must specifications (which should never be violated) and desirable specifications (the violation of which may be unavoidable). In this paper, we propose a method for synthesizing a reactive system that realizes all must specifications and strongly endeavors to satisfy each desirable specification. The general form of the desirable specifications without assumptions is $$\mathbf{G }\varphi $$ , which means “ $$\varphi $$ always holds”. In our approach, the best effort to satisfy $$\mathbf{G }\varphi $$ is to maximize the number of steps satisfying $$\varphi $$ in the interaction. To quantitatively evaluate the number of steps, we used a mean-payoff objective based on LTL formulae. Our method applies the Safraless approach to construct safety games from given must and desirable specifications, where the must specification can be written in full LTL and may include assumptions. It then transforms the safety games constructed from the desirable specifications into mean-payoff games and finally composes a reactive system as an optimal strategy on a synchronized product of the games.

In this article we propose a novel formalism to model and analyse gene regulatory networks using a well-established formal verification technique. We model the possible behaviours of networks by logical formulae in linear temporal logic (LTL). By checking the satisfiability of LTL, it is possible to check whether some or all behaviours satisfy a given biological property, which is difficult in quantitative analyses such as the ordinary differential equation approach. Owing to the complexity of LTL satisfiability checking, analysis of large networks is generally intractable in this method. To mitigate this computational difficulty, we developed two methods. One is a modular checking method where we divide a network into subnetworks, check them individually, and then integrate them. The other is an approximate analysis method in which we specify behaviours in simpler formulae which compress or expand the possible behaviours of networks. In the approximate method, we focused on network motifs and presented approximate specifications for them. We confirmed by experiments that both methods improved the analysis of large networks.

Verifying realizability in the specification phase is expected to reduce the development costs of safety-critical reactive systems. If a specification is not realizable, we must correct the specification. However, it is not always obvious what part of a specification should be modified. In this paper, we propose a method for obtaining the location of flaws. Rather than realizability, we use strong satisfiability, due to the fact that many practical unrealizable specifications are also strongly unsatisfiable. Using strong satisfiability, the process of analyzing realizability becomes less complex. We define minimal strongly unsatisfiable subsets (MSUSs) to locate flaws, and construct a procedure to compute them. We also show correctness properties of our method, and clarify the time complexity of our method. Furthermore, we implement the procedure, and confirm that MSUSs are computable for specifications of reactive systems at non-trivial scales.

We developed a method for analyzing the dynamics of gene regulatory networks in purely qualitative fashion. In our method, constraints for possible behaviors of a network and a biological property of interest are described as Linear Temporal Logic formulas, being automatically analyzed by satisfiability checking. In this way, we can investigate whether there exists some behavior which satisfies a specified property or whether all the behaviors satisfy a specified property, which are difficult in quantitative analysis.

Many fatal accidents of safety critical reactive systems have occurred in unexpected situations which had not been considered during the design and test phases of the systems. To prevent these accidents, reactive systems should be designed to respond appropriately to any requests of any timing from environments. Verifying this property at specification phase reduces the development costs of safety critical reactive systems. This property of a specification is well known as realizability. If a specification was found not to be realizable, we have to determine the flaws in the unrealizable specification. Unrealizability of a specification arises from arbitrary requirements given by system designers. From a different view, it can be thought that the unrealizable specification implicitly imposes a precondition on the behavior of environment, although a system can not control the behavior of environment. If it is possible to obtain the precondition in intuitively comprehensive forms, it is easy for system designers to understand the cause of flaws in specifications. In this paper, we propose methods for deriving constraints on the behavior of environments, which is implicitly imposed by unrealizable specifications. Instead of realizability, we use strong satisfiability which is a necessary condition for realizability, due to the fact that many practical unrealizable specifications are also strongly unsatisfiable, and strong satisfiability have the advantage of lower complexity for analysis against realizability. These methods derive constraints in propositional linear temporal logic from Buchi automata representing specifications. The expressions of derived constraints are limited to simple and intuitively comprehensive forms where only two temporal operators appear successively. We also give proofs for three correctness properties of our methods, i.e. the termination property, the soundness property, and the weakest constraints derivability. Finally, we discuss applicability of our methods.