Searching for invariants using temporal resolution

DOI10.1007/3-540-36078-6_6MaRDI QIDQ4428293zbMATH OpenFDO

Authors James Brotherston, Anatoli I. Degtyarev, Michael Fisher, Alexej P. Lisitsa

Publication date 15 September 2003

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/2514/25140086.htm

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Invariant-free clausal temporal resolution
• Algorithms for guiding clausal temporal resolution
• scientific article; zbMATH DE number 67448
• Search strategies for resolution in temporal logics
• Temporal resolution using a breadth-first search algorithm

Cited in

(5)

• Extracting mutual exclusion invariants from lifted temporal planning domains
• Invariant template matching in systems with spatiotemporal coding: a matter of instability
• Constraint-based algorithm for computing temporal invariants
• Invariant-free clausal temporal resolution
• On the expressive power of the normal form for branching-time temporal logics

This page was built for publication: Searching for invariants using temporal resolution

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