A verifier for distributed real-time systems with bounded integer variables

The authors propose asynchronous register temporal logic (ARTL), which is suitable for the specification and verification of distributed real-time software systems. ARTL adopts a multiclock model that has no explicit reference to global time and, unlike other propositional temporal logics, has a built-in capability for reasoning about bounded integer variables, called registers, together with a freezing modal operator for fixing register contents. The implementation and experimentation of a verifier for ARTL based on the tableau method are described. The tableau method for ARTL is discussed. The verifier was tested against several benchmarks with good results. Since the satisfiability problem for ARTL is EXPSPACE-hard, several strategies for improving the efficiency of the tableau method have been implemented and are considered