TY - GEN

T1 - Using locales to define a rely-guarantee temporal logic

AU - Mansky, William

AU - Gunter, Elsa

PY - 2012/9/5

Y1 - 2012/9/5

N2 - In this paper, we present an agent-based logic called Rely-Guarantee Temporal Logic (RGTL), developed using the Isabelle theorem prover. RGTL provides a formalism for expressing complex temporal-logic specifications of multi-agent systems, as well as a compositional method of reasoning about the dependencies between components in such a system. Taking advantage of Isabelle's locale functionality, we are able to express various choices about the notion of "strategy" used in the logic (e.g., memoryless/memory-based) as parameters to the semantics, whereas previously these choices were considered to define semantics for distinct variants of agent-based logics. We can then state and formally verify various aspects of RGTL, including its reasoning principles and its expressiveness relative to Alternating-time Temporal Logic (ATL), independently of the type of underlying strategies, by using locales to axiomatize the necessary requirements on strategies.

AB - In this paper, we present an agent-based logic called Rely-Guarantee Temporal Logic (RGTL), developed using the Isabelle theorem prover. RGTL provides a formalism for expressing complex temporal-logic specifications of multi-agent systems, as well as a compositional method of reasoning about the dependencies between components in such a system. Taking advantage of Isabelle's locale functionality, we are able to express various choices about the notion of "strategy" used in the logic (e.g., memoryless/memory-based) as parameters to the semantics, whereas previously these choices were considered to define semantics for distinct variants of agent-based logics. We can then state and formally verify various aspects of RGTL, including its reasoning principles and its expressiveness relative to Alternating-time Temporal Logic (ATL), independently of the type of underlying strategies, by using locales to axiomatize the necessary requirements on strategies.

KW - Isabelle proof assistant

KW - logics for agency

KW - modular specification

KW - reasoning about strategies

KW - temporal logic

UR - http://www.scopus.com/inward/record.url?scp=84865574621&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84865574621&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-32347-8_20

DO - 10.1007/978-3-642-32347-8_20

M3 - Conference contribution

AN - SCOPUS:84865574621

SN - 9783642323461

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 299

EP - 314

BT - Interactive Theorem Proving - Third International Conference, ITP 2012, Proceedings

T2 - 3rd International Conference on Interactive Theorem Proving, ITP 2012

Y2 - 13 August 2012 through 15 August 2012

ER -