A modal logic-based model of traffic system

A hybrid system in which continuous and discrete variables are involved is drawing much attention of researchers in system control. Traffic control system can be regarded as a typical example of hybrid system since both continuous variables such as a number of cars, speeds, and discrete ones, for example, traffic signals and so on are involved in the system. For modeling of the hybrid system, there exist various approaches based on discrete event system theory, which utilizes mainly timed automaton, Petri net and so forth. The traffic control system can be also regarded as a 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, we take a simple traffic system as an example, propose one of the modeling methods using modal logic and consider its applicability to control.