Using Locales to Define a Rely-Guarantee Temporal Logic

DOI10.1007/978-3-642-32347-8_20MaRDI QIDQ2914750zbMATH OpenOpenAlexFDO

Authors William Mansky, Elsa Gunter

Publication date 20 September 2012

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-32347-8_20

zbMATH Keywords

Isabelle proof assistantlogics for agencymodular specificationreasoning about strategiestemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in artificial intelligence (68T27) Agent technology and artificial intelligence (68T42)

Recommendations

• Temporal logics with local constraints (invited talk)
• Temporal logics for the specification of performance and reliability
• Local rely-guarantee reasoning
• scientific article; zbMATH DE number 2086683
• Assumption/guarantee specifications in linear-time temporal logic
• Specification and verification using temporal logics
• Reified temporal logics: An overview
• Implementing Temporal Logics: Tools for Execution and Proof
• On using temporal logic for refinement and compositional verification of concurrent systems
• Assumption/guarantee specifications in linear-time temporal logic (extended abstract)

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Using Locales to Define a Rely-Guarantee Temporal Logic

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