Research On Intuitionistic Temporal Logic

It is well known that reactive systems often engage in ongoing and non-terminating interaction with environment,their behavior are usually infinite. On the other hand, run-time verification is a lightweight verification technology, which need to determine whether the finite observations violate the given specification or not according to the current behavior of system.Clearly,finite behavior is involved in run-time verification.Temporal logic is one of the most important formalisms used to describe the properties of reactive systems,in order to capture properties of finite and infinite behaviors in unifying framework,different interpretations of temporal logic have been introduced,among them,Patrick Maier provided the intuitionistic temporal logic.The paper aims at exploring safety,liveness and iterated Boolean games in intuitionistic temporal logic. Main work includes:1. Present intuitionistic computing tree logic called ICTL,and compare the expressive power between CTL and ICTL.2. Introduce and explore the notions of universally and existentially safety and liveness in ICTL,study the closure properties of safety and liveness under the operations disjunction,conjunction,negation and so on.3. The decomposition theorem about ICTL is established,and the relationships of safety and liveness in logics ILTL,ICTL and CTL are explored.4. In the framework of intuitionistic linear temporal logic,we consider some issues on iterated Boolean games including:the relation between the satisfiability of player's goal and strategy profiles of iterated Boolean games,and the relation of ILTL formulas and Nash equilibria strategy profiles.