R.A. Brualdi, A.J. Hoffman
Linear Algebra and Its Applications
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.
R.A. Brualdi, A.J. Hoffman
Linear Algebra and Its Applications
Donald Samuels, Ian Stobert
SPIE Photomask Technology + EUV Lithography 2007
Ehud Altman, Kenneth R. Brown, et al.
PRX Quantum
Tong Zhang, G.H. Golub, et al.
Linear Algebra and Its Applications