logics for model checking

["Wojtowicz, Ralph" <wojtowicz@metsci.com>]

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