* Re: logics for model checking
@ 2008-09-02 18:07 Claudio Hermida
0 siblings, 0 replies; 3+ messages in thread
From: Claudio Hermida @ 2008-09-02 18:07 UTC (permalink / raw)
To: categories
Wojtowicz, Ralph wrote:
> Finally, here are a few questions.
>
> Has anyone studied the model-checking logics using the tools
> of categorical logic?
>
>
Here's a little note I wrote about relational modalities from a
categorical logic viewpoint; it includes a few further references which
may be relevant to your question
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.3240
Claudio Hermida
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: logics for model checking
@ 2008-09-03 20:59 Luigi Santocanale
0 siblings, 0 replies; 3+ messages in thread
From: Luigi Santocanale @ 2008-09-03 20:59 UTC (permalink / raw)
To: categories
Hi,
> Any other thoughts, suggestions, or references would be
> appreciated.
In
L. S. Completions of \mu-algebras. APAL, 154(1):27-50, May 2008.
I studied the problem of the completeness of the modal mu-calculus from
an finitary algebraic point of view. In that paper some categorical
ideas, mainly from
W. Tholen, Pro-categories and multiadjoint functors, Canad. J. Math. 36
(1) (1984) 144–155.
play the relevant role. The challenge is to prove that in free modal
\mu-algebras, the relation
\mu.f = \bigvee_{n>=0} f^n(\bot)
holds -- where \mu.f, the least fixpoint of f, is axiomatized by
equational implications and free modal \mu-algebras are not known to be
complete.
Best,
Luigi
--
Luigi Santocanale
LIF/CMI Marseille Tél: 04 91 11 35 74
http://www.cmi.univ-mrs.fr/~lsantoca/ Fax: 04 91 11 36 02
^ permalink raw reply [flat|nested] 3+ messages in thread
* logics for model checking
@ 2008-09-02 14:24 Wojtowicz, Ralph
0 siblings, 0 replies; 3+ messages in thread
From: Wojtowicz, Ralph @ 2008-09-02 14:24 UTC (permalink / raw)
To: categories
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
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2008-09-03 20:59 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2008-09-02 18:07 logics for model checking Claudio Hermida
-- strict thread matches above, loose matches on Subject: below --
2008-09-03 20:59 Luigi Santocanale
2008-09-02 14:24 Wojtowicz, Ralph
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).