Complete Proof System for QPTL

DOI10.1093/logcom/12.5.701zbMath1013.03012OpenAlexW2086950378MaRDI QIDQ4779585

Amir Pnueli, Yonit Kesten

Publication date: 21 June 2003

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/966b905778116a4844bb87d02a2eaea5d3f38d6e

zbMATH Keywords

completenesstemporal logicrefinementBüchi automataaxiomatic systemflexible variableshistory schemeprophecy schemerigid variable

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Related Items (11)

Functional Specification of Hardware via Temporal Logic ⋮ Model-checking iterated games ⋮ The refinement calculus of reactive systems ⋮ A proof system for unified temporal logic ⋮ A sound and complete proof system for a unified temporal logic ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Propositional Dynamic Logic with Program Quantifiers ⋮ A novel approach to verifying context free properties of programs ⋮ Tool support for learning Büchi automata and linear temporal logic ⋮ Propositional Dynamic Logic for Hyperproperties ⋮ A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time

This page was built for publication: Complete Proof System for QPTL