We address a path planning problem for heterogeneous multi-robot systems under specifications consisting of temporal constraints and routing tasks such as package delivery services. The robots are partitioned into several groups based on their dynamics and specifications. We introduce a concise description of such tasks, called a work, and extend counting LTL to represent such specifications. We convert the problem into an ILP problem. We show that the number of variables in the ILP problem is fewer than that of the existing method using cLTL+. By simulation, we show that the computation time of the proposed method is faster than that of the existing method.

In a multi-agent system, it is important to consider a design method of cooperative actions in order to achieve a common goal. In this paper, we propose two novel multi-agent reinforcement learning methods, where the control specification is described by linear temporal logic formulas, which represent a common goal. First, we propose a simple solution method, which is directly extended from the single-agent case. In this method, there are some technical issues caused by the increase in the number of agents. Next, to overcome these technical issues, we propose a new method in which an aggregator is introduced. Finally, these two methods are compared by numerical simulations, with a surveillance problem as an example.

In spatially distributed systems such as smart buildings and intelligent transportation systems, control of spatio-temporal patterns is an important issue. In this paper, we consider a finite-horizon optimal spatio-temporal pattern control problem where the pattern is specified by a signal spatio-temporal logic formula over finite traces, which will be called an SSTLf formula. We give the syntax and Boolean semantics of SSTLf. Then, we show linear encodings of the temporal and spatial operators used in SSTLf and we convert the problem into a mixed integer programming problem. We illustrate the effectiveness of this proposed approach through an example of a heat system in a room.

This paper presents a novel method for optimal control of timed Petri nets, introducing a novel temporal logic based constraint called a generalized mutual exclusion temporal constraint (GMETC). The GMETC is described by a metric temporal logic (MTL) formula where each atomic proposition represents a generalized mutual exclusion constraint (GMEC). We formulate an optimal control problem of the timed Petri nets under a given GMETC and solve the problem by transforming it into an integer linear programming problem where the MTL formula is encoded by linear inequalities. We show the effectiveness of the proposed approach by a numerical simulation.

We address a BEMS (Building Energy Management System) to guarantee reliability of electric-power supply in dynamic uncertain environments. The building microgrid as the target of BEMS has multiple distributed power sources including a photo-voltaic power system and Electric-Vehicle (EV). EV is regarded as an autonomously-moving battery due to the original means of transportation and is hence a cause of dynamic uncertainty of the building microgrid. The main objective of synthesis of BEMS in this paper is to guarantee the continuous supply of power to the most critical load in a building microgrid and to realize the power supply to the other loads according to a ranking of load importance. We synthesize the BEMS as a reactive control system that monitors changes of dynamic uncertain environment of the microgrid including departure and arrival of an EV, and determines a route of power supply to the most critical load. Also, we conduct numerical experiments of the reactive BEMS using models of power flows in the building and of charging states of the batteries. The experiments are incorporated with data measured in a practical office building and demonstration project of EMS at Osaka, Japan. We show that the BEMS works for extending the time duration of continuous power supply to the most critical load.

In this paper, we study a control problem of a concurrent discrete event system, where several subsystems are partially synchronized via shared events, under local and global constraints described by linear temporal logic formulas. We propose a hierarchical control architecture consisting of local supervisors and a coordinator. While the supervisors ensure the local requirements, the coordinator decides which shared events to be disabled so as to satisfy the global specification. First, we construct Rabin games to obtain local supervisors. Next, we reduce them based on shared transitions. Finally, we construct a global Rabin game from the reduced supervisors and a deterministic Rabin automaton that accepts every run satisfying the global specification. By solving it, we obtain a coordinator that disables shared events to guarantee the global requirement. Moreover, the concurrent system controlled by the coordinator and the local supervisors is deadlock-free.

Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic. We relax the problem so that if the verification process cannot succeed at the prescribed precision, it outputs an inconclusive result. The problem is solved by an efficient and rigorous monitoring algorithm. This algorithm performs a forward simulation of a continuous-time dynamical system, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. In each step, the continuous state at a certain time is enclosed by an interval vector that is proven to contain a unique solution. We experimentally demonstrate the utility of the proposed method in formal analysis of nonlinear and complex continuous systems.

In this paper, optimal control of multi-vehicle systems is studied. In the case where collision avoidance between vehicles and obstacle avoidance are imposed, state discretization is effective as one of the simplified approaches. Furthermore, using state discretization, cooperative actions such as rendezvous can be easily specified by linear temporal logic (LTL) formulas. However, it is not necessary to discretize all states, and partial states (e.g., the position of vehicles) should be discretized. From this viewpoint, a new control method for multi-vehicle systems is proposed in this paper. First, the system in which partial states are discretized is formulated. Next, the optimal control problem with constraints described by LTL formulas is formulated, and its solution method is proposed. Finally, numerical simulations are presented. The proposed method provides us a useful method in control of multi-vehicle systems.

The algebra of communicating shared resources (ACSR) is a timed process algebra which extends classical process algebras with the notion of a resource. In analyzing ACSR models, the existing techniques such as bisimulation checking and Hennessy-Milner Logic (HML) model checking are very important in theory of ACSR, but they are difficult to use for large complex system models in practice. In this paper, we suggest a framework to verify ACSR models against their requirements described in an expressive timed temporal logic. We demonstrate the usefulness of our approach with a real world case study.

Workflow nets (WF-nets) are Petri nets which represent workflows. Soundness is a criterion of logical correctness defined for WF-nets. It is known that soundness verification is intractable. In this paper, we propose a method to verify soundness using a Linear Temporal Logic (LTL) model checking tool, SPIN. We give an LTL necessary and sufficient condition to verify soundness for WF-nets without livelock. Acyclic WF-nets have no livelock, but cyclic WF-nets may have livelock. We also give a necessary and sufficient condition to verify livelock. Meanwhile, we show that any LTL model checking tool cannot verify soundness for WF-nets with livelock. We give necessary conditions to verify soundness for them. Those conditions enable us to use SPIN even if a given WF-net has livelock. We also develop a tool to verify soundness based on our method. We show effectiveness of our method by comparing our tool with existing soundness verification tools on verification time for 200 cyclic ACWF-nets.

Input/Output (I/O) automata and the Temporal Logic of Actions (TLA) are two well-known techniques for the specification and verification of concurrent systems. Over the past few years, they have been extended to the so-called dynamic I/O automata and, respectively, Mobile TLA (MTLA) in order to be more appropriate for mobile agent systems. Dynamic I/O automata is just a mathematical model, whereas MTLA is a logic with a formally defined language. In this paper, therefore, we investigate how MTLA could be used as a formal language for the specification of dynamic I/O automata. We do this by writing an MTLA specification of a travel agent system which has been specified semi-formally in the literature on that model. In this specification, we deal with always existing agents as well as with an initially unknown number of dynamically created agents, with mobile and non-mobile agents, with I/O-automata-style communication, and with the changing communication capabilities of mobile agents. We have previously written a TLA specification of this system. This paper shows that an MTLA specification of such a system can be more elegant and faithful to the dynamic I/O automata definition because the agent existence and location can be expressed directly by using agent and location names instead of special variables as in TLA. It also shows how the reuse of names for dynamically created and destroyed agents within the dynamic I/O automata framework can be specified in MTLA.

We propose a new tableau construction which builds an FSM, instead of a Kripke structure, from a formula in a class of temporal logic named ASTL. This FSM is a maximal model of the formula under the preorder derived from simulation relations. Additionally, we propose a method using the tableaus to build controllers in a certain topology of interconnected FSMs. We can use ASTL to describe the desired behaviors of the control system. This method is applicable to generating digital circuits. Moreover, this method accepts a wider range of specifications than conventional methods.

This paper considers systems consisting of communicating processes which can move between specified locations. Mobile telephone systems and intelligent transport systems are examples of them. The processes can exchange data as well as channels (e.g. frequencies) to be used in further communication. It may happen that two processes (e.g. telephones or cars) in different locations could communicate directly because they share a communication channel, but they cannot as there is a physical obstacle between the locations. A possible solution is to allow one process to send a message to another one through other processes and locations. To see if this is possible, a notion of connectivity of processes has been devised in the literature. A process was defined to be connectable to another one if a message from the first one could reach the other one by using any existing communication actions, allowed locations, and process moves in the system. A process-algebraic approach for checking connectivity was proposed. In this paper, it is shown how the temporal logic of actions (TLA) can be employed for the same purpose. In both approaches, connectivity of a process with another one is basically checked as follows. The first process includes a marking message in all its sending actions. Every process that receives this message gets marked and includes it in its own sending actions. The first process is connectable to the second one if there exists such a system execution sequence that the latter gets marked in it. Since TLA is a linear-time temporal logic, it can generally not express such a property. This paper, however, shows that it can be expressed and verified for a given TLA system specification. It also shows how to specify the marking operations and provides an example of connectivity checking.

This paper introduces a probabilistic modeling of alarm observation delay, and shows a novel method of model-based diagnosis for time series observation. First, a fault model is defined by associating an event tree rooted by each fault hypothesis with probabilistic variables representing temporal delay. The most probable hypothesis is obtained by selecting one whose Akaike information criterion (AIC) is minimal. It is proved by simulation that the AIC-based hypothesis selection achieves a high precision in diagnosis.

Critical properties of real-time embedded systems must be verified before these systems are deployed as failing to meet these properties may cause considerable property damages and/or human casualties. Although Statechart is one of the most popular languages for modeling behavior of real-time systems, proof systems and analysis tools for Statechart so far are in research and do not fully support the semantics of the original Statechart, or have limited capabilities for proving real-time properties. This paper introduces a toolset ASADAL/PROVER for verifying temporal properties of Statechart extended with justice and compassion properties. ASADAL/PROVER is composed of two subsystems, RTTL-Prover and Model-Checker. The RTTL-Prover converts Statechart specifications into real-time temporal logic (RTTL) formulas of Ostroff, and then checks if the formulas satisfy a temporal property (also in RTTL) using theorem proving techniques. The Model-Checker supports verification of a predefined set of real-time properties using a model checking technique. The RTTL-Prover can support verification of any real-time properties as long as they can be specified in RTTL and, therefore, messages generated by the tool are general and may not be of much help in debugging Statechart specifications. The Model-Checker, however, can provide detailed information for debugging. ASADAL/PROVER has been applied successfully to some experimental systems. One of on-going researches in this project is to apply the symbolic model-checking technique by[3]to support Statecharts with a much larger global-state space. We are also extending the types of temporal properties supported by the Model-Checker.

Support of collaborative work and management of spatio-temporal data has become one of the most interesting and important database applications, which is due to the tremendous progress of database and its surrounding technologies in the last decade. In this paper, we investigate the new generation database technologies that are needed to support such advanced applications. Because of the recent progress of virtual reality technology, virtual work spaces are now available. We examine a typical CSCW (Computer Supported Cooperative Work) fsystem to identify database problems that arise from it. We introduce typical approaches to database improvement based on the high-level view and the virtual reality technique. Also, in this paper, the following are introduced and discussed: the design and implementation of three- and four-dimensional spatio-temporal database systems, VRML (Virtual Reality Modeling Language) database systems, fast access methods to spatio-temporal data, and the interval-based approach to temporal multimedia databases.

We present a topological framework of stepwise specification for concurrent systems in this paper. Some of description techniques can make topologies on the system space. Such topologies corresponds to abstract levels of those description techniques. Using a family of such description techniques, one can specify systems stepwisely. This framework allows to bridge various DTs and modularizing, so that global properties and module properties of systems become to be related to each other. Within this framework, we show derivation of a LOTOS cpecification from temporal logic formulae. An extended version of LOTOS with respect to concurrency is used in this paper. A semantics including concurrency is introduced to do this in this method. The method presented in this paper is applied to mobile telecommunication.

A typed, object-oriented database technology, equipped with appropriate declarative, temporal logic based executable constraints, is presented. The underlying object-oriented database type system is based on advanced features such as subtype, parametric and F-bounded polymorphism. A particularly distinctive feature of the type system is its associated type-safe reflection technology, which provides the flexibility required by database operators without sacrificing type safety. Strongly, and even statically typed, executable class specifications of a variety of standard database abstractions, both application-oriented and system-oriented, are presented in the paper, in order to demonstrate strate the applicability of the paradigm. The temporal logic basis of the constraint language has an execution model, as well as the minimal model semantics, and it allows complex, temporal behavioral patterns to be expressed. It is based on three tomporal operators: always, next time and some time, and rules that determine how these operators may be applied in temporal Horn clauses. Because of the object-oriented nature of the paradigm, the logic basis is also equipped with the equality predicate The proposed technology is intended to provide major advantages not only in managing appropriately complex application environments with temporal constraints, but also in providing more efficient (because of static type checking) and reliable database management systems. It offers the advantages of non-procedural data languages and the richness of a temporal object-oriented paradigm. It also leads to a powerful prototyping tool for structural and behavioral testing of complex, strongly typed object-oriented systems, prior to major procedural implementation efforts.

This paper presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model checker. Using this method, we have verified a model of an aircraft control system with 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.

In this paper we propose a method of formal verfication of fault-tolerance of sequential machines using regular temporal logic. In this method, fault-tolerant properties are described in the form of input-output sequences in regular temporal logic formulas and they are formally verified by checking if they hold for all possible input-output sequences of the machine. We concretely illustrate the method of its application for formal verification of fail-safeness with an example of a comparator for redundant system. The result of verification shows effectiveness of the proposed method.