Hybrid Systems and the Modal Mu-Calculus

摘要

Much of the contemporary work in logics for the formal verification of hybrid systems (notably the work of Henzinger at UC Berkeley and Manna at Stanford) builds directly on the framework of temporal logic verification of discrete systems. The core computational model is that of a hybrid automaton, which is represented formally as a transition system over a hybrid state space X subset contained in Q x IR(n), where Q is a finite set of discrete modes. While the temporal logic framework is adequate to formally express many qualitative dynamic properties of such systems, it fails to capture the 'continuity' of continuous dynamics, or to reflect the topological and metric structure of Euclidean space. In addressing this deficiency, we look to the modal mu- calculus, a richly expressive formal logic over transition system models, into which virtually all temporal and modal logics can be translated. The key move in this paper is to view the transition system models of hybrid automata not merely as some form of 'discrete abstraction', but rather as a skeleton which can be fleshed out by imbuing the state space with topological, metric tolerance or other structure. Drawing on the resources of modal logics, we give explicit symbolic representation to such structure in polymodal logics extending the modal mu-calculus.