Formula Clock Automata

Finite automata are instrumental for the modeling and analysis of many phenomenon within computer science. In particular, automata theory plays an important role in the verification of concurrent finite-state systems. But it can only describe the sequence by which the events of system happen . It can't exactly express the delay between various events and the timed requirements. In order to capture the timed requirements of real-time system's behaviors, people proposed timed automata. Timed automata is obtained by adding a notion of time to automata and often being used to model the behaviors of real-time system. Verification of a real-time system consists in checking whether the implementation of the system satisfies a set of required properties, we use timed automata AI to model the implementation and AS to model the properties.In order to verify, we only need to decide whether the language accepted by AI is contained in the language accepted by As. If As is deterministic, the problem can be solved in PSPACE, however, if As is nondeterministic, the problem is undecidable.We proposed formula-clock automata based on profound learning and analysising timed automata. In the formula-clock automata , an event correspond to a proposition and we define two clocks: formula-recording clock and formula-predicting clock for every linear propositional temporal logic formula which is based on the given set of propositons. The former records the elapse of time from the latest moment at which the formula corresponding the clock was satisfied, while the latter predicts the next moment at which the formula corresponding the clock will be satisfied. At the same time , we discuss the determinism and nondeterminism of formula-clock automata and the closure propertied under Boolean operation of the language which is accepted by formula-clock automata. We also prove the expressive equivalence between the deterministic formula-clock automata and the nondeterministic formula-clock automata. This means that every nondeterministic formula-clock automata can be transformed to a deterministic formula-clock automata which exactly accept the timed language identified by the fomer.We alsoextend timed words to infiniteness and define the formula-clock Buchi automata and the formula-clock Muller automata. At last, we show its application in formal verification and modeling of real-time system.