Heinz Koeppl, Marc Hafner, et al.
BMC Bioinformatics
We consider the computation tree logic (CTL) proposed in (Sci. Comput. Programming 2 (1982), 241-260) which extends the unified branching time logic (UB) of ("Proc. Ann. ACM Sympos. Principles of Programming Languages, 1981," pp. 164-176) by adding an until operator. It is established that CTL has the small model property by showing that any satisfiable CTL formulae is satisfiable in a small finite model obtained from the small "pseudomodel" resulting from the Fischer-Ladner quotient construction. Then an exponential time algorithm is given for deciding satisfiability in CTL, and the axiomatization of UB given in ibid. is extended to a complete axiomatization for CTL. Finally, the relative expressive power of a family of temporal logics obtained by extending or restricting the syntax of UB and CTL is studied. © 1985.
Heinz Koeppl, Marc Hafner, et al.
BMC Bioinformatics
W.C. Tang, H. Rosen, et al.
SPIE Optics, Electro-Optics, and Laser Applications in Science and Engineering 1991
Timothy J. Wiltshire, Joseph P. Kirk, et al.
SPIE Advanced Lithography 1998
Fausto Bernardini, Holly Rushmeier
Proceedings of SPIE - The International Society for Optical Engineering