Using locales to define a rely-guarantee temporal logic

William Mansky, Elsa Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationInteractive Theorem Proving - Third International Conference, ITP 2012, Proceedings
Number of pages16
StatePublished - Sep 5 2012
Event3rd International Conference on Interactive Theorem Proving, ITP 2012 - Princeton, NJ, United States
Duration: Aug 13 2012Aug 15 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7406 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other3rd International Conference on Interactive Theorem Proving, ITP 2012
Country/TerritoryUnited States
CityPrinceton, NJ


  • Isabelle proof assistant
  • logics for agency
  • modular specification
  • reasoning about strategies
  • temporal logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Using locales to define a rely-guarantee temporal logic'. Together they form a unique fingerprint.

Cite this