A formalization of real-time system using modal logic

Traffic control systems are typical examples of hybrid systems as both continuous and discrete variables, such as the number of cars, their speeds and traffic signals, are involved in the system. For the modeling of hybrid systems, there exist various approaches based on the discrete event system theory, which utilizes, for example, timed automaton, Petri net and so forth. The traffic control system can often be regarded as the system controlled by a logic-based controller. In addition, if the control specifications are also given by logical expressions, it may not be difficult to modify the existing logic-based controller. In this paper, the traffic control system consisting of two crossings is taken as an example, one of the modeling methods using modal logic is proposed, and its applicability to control is considered.