AXIOMATIZATIONS OF TEMPORAL LOGICS ON TRACE SYSTEMS

Article type: Research Article

Authors: Penczek, Wojciech

Affiliations: Institute of Computer Science, Polish Academy of Sciences, Warsaw, ul. Ordona 21, Poland email: penczek@ipipan.waw.pl

Note: [] Partly supported by the KBN grant No. 8 Tl1C 029 08.

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.

DOI: 10.3233/FI-1996-25204

Journal: Fundamenta Informaticae, vol. 25, no. 2, pp. 183-200, 1996