Formal reasoning about actor programs using temporal logic

DOI10.1007/3-540-45397-0_18MaRDI QIDQ2761739zbMATH OpenFDO

Authors Susanne Schacht

Publication date 7 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2001/20010445

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computing methodologies and applications (68U99)

Review text

We here present an approach to reasoning about actor programs on the basis of temporal logic. Temporal logic is particularly appropriate for the specification of concurrent programs, but most known temporal logic proof systems for concurrent computations rely on imperative language constructs, ignoring, e.g., the creation of processes and the dynamic configuration of communication channels, which are crucial for actor based programming. We will demonstrate our approach by applying it to a detection algorithm for termination of parts of a computation. For the entire collection see [Zbl 0976.68544].

Recommendations

• Temporal reasoning about actor programs
• scientific article; zbMATH DE number 2087421
• Proving correctness of timed concurrent constraint programs
• scientific article; zbMATH DE number 4081518
• Temporal logic based static analysis for non-uniform behaviours.

Cited in

(6)

• Modeling actor systems using dynamic I/O automata
• Proof-theoretic foundations for the design of actor systems
• Temporal reasoning about actor programs
• Reasoning about programs by exploiting the environment
• scientific article; zbMATH DE number 2182600 (Why is no real title available?)
• Temporal logic based static analysis for non-uniform behaviours.

This page was built for publication: Formal reasoning about actor programs using temporal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2761739)