Automatic verification of Golog programs via predicate abstraction

DOI10.3233/978-1-61499-672-9-760MaRDI QIDQ4576210zbMATH OpenFDO

Authors Peiming Mo, Naiqi Li, Yong-Mei Liu

Publication date 12 July 2018

Full work available at URL https://doi.org/10.3233/978-1-61499-672-9-760

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of Golog programs over description logic actions
• On the verification of very expressive temporal properties of non-terminating Golog programs
• Verifying CTL\(^\ast\) properties of \textsc{Golog} programs over local-effect actions
• Predicate abstraction for program verification
• Decidable verification of decision-theoretic Golog

Cited in

(5)

• Situation calculus for controller synthesis in manufacturing systems with first-order state representation
• On the verification of very expressive temporal properties of non-terminating Golog programs
• Verifying CTL\(^\ast\) properties of \textsc{Golog} programs over local-effect actions
• scientific article; zbMATH DE number 6606377 (Why is no real title available?)
• Abstracting situation calculus action theories

Describes a project that uses

Uses Software

• GOLOG

This page was built for publication: Automatic verification of Golog programs via predicate abstraction

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