Abstraction-based verification of infinite-state reactive modules

DOI10.3233/978-1-61499-672-9-725MaRDI QIDQ4576204zbMATH OpenOpenAlexFDO

Authors Francesco Belardinelli, Alessio Lomuscio

Publication date 12 July 2018

Full work available at URL https://spiral.imperial.ac.uk/bitstream/10044/1/50041/9/FAIA285-0725.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Agent technology and artificial intelligence (68T42)

Recommendations

• Model checking auctions as artifact systems: decidability via finite abstraction
• Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
• scientific article; zbMATH DE number 6902518
• Automatic data-abstraction in model checking multi-agent systems
• Deductive verification of alternating systems

Cited in

(6)

• Hybrid verifications of reactive programs
• Abstracting and Verifying Strategy-Proofness for Auction Mechanisms
• Model checking auctions as artifact systems: decidability via finite abstraction
• Alternating-time temporal logic with default actions
• Formal verification and synthesis of mechanisms for social choice
• Towards imperative modules: reasoning about invariants and sharing of mutable state

This page was built for publication: Abstraction-based verification of infinite-state reactive modules

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