I am trying to understand model-checking logics such as linear temporal logic (LTL), computation tree logic (CTL), and probabilistic extensions such as probabilistic computation tree logic (PCTL). These logics seem to be useful in model- checking because of correspondences between recursive definitions of formulas and recursive algorithms for computing them. Syntactic inference and any semantics other than the few (transition systems, DTMCs, MDPs, etc.) for which the logics were developed seem not to be of interest, however. Translation theorems such as D1.4.7, D1.4.12, and D4.3.13 of Johnstone's "Elephant" are not applied, as far as I have found. Here are some initial thoughts based on my very limited knowledge of categorical logic. The temporal logic operators "next", "eventually", and "always" may, for example, be formulated using a propositional signature. Let A be a set whose elements are thought of as state labels. The set of atomic propositions is {a_n | a in A, n in N}. The following are Horn formulas: Next^n[a] = a_n Always^k[a] = a_0 \wedge ... \wedge a_k T^k[a, b] = a_0 \wedge ... \wedge a_{k-1} \wedge b_k The following are coherent formulas: Until^k[a, b] = T^0[a, b] \vee ... \vee T^k[a, b] Eventually^k[a] = a_0 \vee ... \vee a_k The following are geometric formulas: Until[a, b] = \vee_i T^i[a, b] Eventually[a] = \vee_i a_i The following is infinitary: Always[a] = \wedge_i a_i. Alternatively, these notions can be formulated as a first-order theory with basic sorts "States" and "Paths". It has function symbols start : Paths -> States shift : Paths -> Paths and a set A of of relation symbols a |-> States. PCTL can be formulated as a \tau-theory. It has basic sorts States and Paths as above as well as the function symbols start and shift. It also has function symbols Prob_{<p}:P(Paths) -> P(States) (similarly for \leq, >, and \geq) for 0 \leq p\leq 1 and Cost_{<c}:P(S) -> P(S) (similarly for \leq, >, and \geq) for 0 \leq c. There are certainly other presentations of these theories. Finally, here are a few questions. Has anyone studied the model-checking logics using the tools of categorical logic? What interactions exist between bisimulation/probabilistic bisimulation and the logics? What role could categorical logic have in developing model- checking algorithms? How can the usual semantics of these theories (e.g., DTMC semantics for PCTL) be viewed categorically (e.g., in the topos Set by interpreting the sorts simply as sets of states and paths)? Any other thoughts, suggestions, or references would be appreciated. References: Arnold. "Finite Transition Systems". Prentice-Hall. 1994. Johnstone. "Sketches of an Elephant: A Topos Theory Compendium". Oxford University Press. 2002. Rutten, Kwiatkowska, Norman, and Parker. "Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems". AMS. 2004. Thanks, Ralph Wojtowicz Metron, Inc. 11911 Freedom Drive, Suite 800 Reston, VA USA wojtowicz@metsci.com