An Asynchronous Automata Approach to the Semantics of Temporal Logic

TL;DR

This paper introduces a novel asynchronous automata framework for understanding the semantics of temporal logic, connecting continuous and discrete time models through differential equations and automaton solutions.

Contribution

It provides a new differential equations-based characterization of asynchronous automata and explores their relation to continuous and discrete temporal logic semantics.

Findings

Differential equations characterize asynchronous automata behavior.

Connection established between continuous and discrete time semantics.

Automaton solutions describe properties of temporal logic formulas.

Abstract

The paper presents the differential equations that characterize an asynchronous automaton and gives their solution x:R->{0,1}x...x{0,1}. Remarks are made on the connection between the continuous time and the discrete time of the approach. The continuous and the discrete time, the linear and the branching temporal logics have the semantics depending on x and their formulas give the properties of the automaton.