Abstract
Partial order temporal logics interpreted on trace systems have been shown not to have finitary complete axiomatizations due to the fact that the complexity of their decidability problem is in II11. This paper gives infinitary complete proof systems for several temporal logics on trace systems e.g. Computation Tree Logic with past operators and an essential subset of Interleaving Set Temporal Logic.
Get full access to this article
View all access options for this article.