Proving Properties of Actor Programs Using Temporal Logic

We here present an approach to reasoning about actor programs on the basis of temporal logic. Temporal logic is particularly appropriate for reasoning about concurrent programs, but most known temporal logic proof systems for concurrent computations rely on imperative language constructs, ignoring, e.g., the creation of processes which is crucial for actor based programming. We will demonstrate our approach by applying it to the partial termination of a series of actor computations. 1 Temporal logic as a tool for program specification and verification Temporal logic is particularly appropriate for reasoning about programs where the operational or denotational semantics is too fine-grained to make useful statements about the overall behavior of a complex system. Using its formal framework safety properties (invariants like partial correctness, absence of deadlock, mutual exclusion etc.) and liveness properties (termination, total correctness, cycles) of concurrent programs can be sho..