<p>The meaning of  <em>simpler</em> in your question is unclear. Kripke structures have a labelling function on states. LTSes have labels on transitions, which can be viewed as a labelling function on transitions. Why is one simpler than the other? In the context of your question, using acronyms like "ACTL" is ambiguous because the "A" could mean <em>all paths</em> or <em>action-based</em>. </p>

<p>The difference, in my opinion, between Kripke structures and LTSes is based on modelling convenience and not simplicity. There is a lot of work comparing and contrasting the two. Here are a few starting points for chasing down related work. </p>

<ol>
<li><p>De Nicola and Vaandrager have a few papers on translating between Kripke structures and LTSes and how this affects logical properties. They introduce doubly labelled transition systems to move between the two types of representations and semantic interpretations. </p>

<p><a href="http://www.springerlink.com/content/y13110781p623363/" rel="nofollow">Action versus state based logics for transition systems </a>, De Nicola and Vaandrager, 1990</p>

<p><a href="http://portal.acm.org/citation.cfm?id=201032" rel="nofollow">Three logics for branching bisimulation</a>, De Nicola and Vaandrager, 1995</p></li>
<li><p>If the goal is verification of event-based systems, one option is to translate the LTS into a Kripke structure and use a Kripke structure model checker. The translation has to preserve the interpretation of CTL over the LTS. </p>

<p><a href="http://dx.doi.org/10.1016/0169-7552%2893%2990047-8" rel="nofollow">An action-based framework for veryfying logical and behavioural properties of concurrent systems</a>, De Nicola, Fantesi, Gnesi, Ristori</p></li>
<li><p>Translating between representations involves a blowup. For the case of LTL, there are cases when this blowup can be avoided. Here is a recent paper on the topic. </p>

<p><a href="http://www.springerlink.com/index/npvpeukpe5nt0gjx.pdf" rel="nofollow">State/event-based software model checking</a>, Chaki, Clarke, Ouaknine, Sharygina, Sinha</p></li>
</ol>

CC BY-SA 3.0
2011-04-21T01:57:46.047Z
Thanks, and yes simpler is probably a bad adjective to attach, maybe I used it because I learned LTSs first so they seem more natural to me but objectively there is no reason why they are simpler. Thanks for the links they do seem to be what I'm looking for.
Camilo
CC BY-SA 3.0
2011-04-20T21:51:04.693Z
2011-04-20T21:51:04.693Z
Vijay D
<p>Normally model checking with specifications written in CTL*/CTL  is done over Kripke structures, however there are ways of doing it over somehow simpler Labelled Transition Systems, for instance <a href="http://www.sciencedirect.com/science?_ob=ArticleURL&amp;_udi=B6V0C-4R335D9-4&amp;_user=10&amp;_coverDate=03%2F15%2F2008&amp;_rdoc=1&amp;_fmt=high&amp;_orig=gateway&amp;_origin=gateway&amp;_sort=d&amp;_docanchor=&amp;view=c&amp;_searchStrId=1721266308&amp;_rerunOrigin=scholar.google&amp;_acct=C000050221&amp;_version=1&amp;_urlVersion=0&amp;_userid=10&amp;md5=178a26820f55526647051e94da181cac&amp;searchtype=a">ACTL</a>. Does anyone has any pointer on similar logics/techniques?</p>

CC BY-SA 3.0
2011-04-18T06:59:20.267Z
It would be easier to answer this question if we knew a bit more about what you already know. Do you know Hennessy-Milner logic? What about the modal $\mu$-calculus? Or ACTL* (http://oai.cwi.nl/oai/asset/1624/1624A.pdf)?
Dave Clarke
CC BY-SA 3.0
2011-04-18T14:11:35.147Z
Dave, I have some notions of μ-calculus and HML, but not any real deep knowledge (which I will have to acquire anyway). For now I'm just looking for reference on time logics applied over LTSs as a starting point.
Camilo
CC BY-SA 3.0
2011-04-18T16:11:00.333Z
See entry: http://cstheory.stackexchange.com/questions/4952/what-are-practically-computable-properties-of-labelled-transition-systems, whose answers should provide you with what you need, including tools working with LTSs such as mCRL and mCRL too.
Dave Clarke
<reference-request><lo.logic><model-checking>
Papers on applying CTL over LTSs
Camilo
# Papers on applying CTL over LTSs

(Asked by: username_0 on 2011-04-18)

Normally model checking with specifications written in CTL\*/CTL is done over Kripke structures, however there are ways of doing it over somehow simpler Labelled Transition Systems, for instance [ACTL](http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6V0C-4R335D9-4&_user=10&_coverDate=03%2F15%2F2008&_rdoc=1&_fmt=high&_orig=gateway&_origin=gateway&_sort=d&_docanchor=&view=c&_searchStrId=1721266308&_rerunOrigin=scholar.google&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=178a26820f55526647051e94da181cac&searchtype=a). Does anyone has any pointer on similar logics/techniques?

**Tags:** reference-request, lo.logic, model-checking

> **Comments:**
> **username_1**: It would be easier to answer this question if we knew a bit more about what you already know. Do you know Hennessy-Milner logic? What about the modal $\mu$-calculus? Or ACTL* (http://oai.cwi.nl/oai/asset/1624/1624A.pdf)?  
> **username_0**: Dave, I have some notions of μ-calculus and HML, but not any real deep knowledge (which I will have to acquire anyway). For now I'm just looking for reference on time logics applied over LTSs as a starting point.  
> **username_1**: See entry: http://cstheory.stackexchange.com/questions/4952/what-are-practically-computable-properties-of-labelled-transition-systems, whose answers should provide you with what you need, including tools working with LTSs such as mCRL and mCRL too.  

---

## 1 answers

### Answer by username_2 on 2011-04-20. Score: 5 | Accepted answer

The meaning of *simpler* in your question is unclear. Kripke structures have a labelling function on states. LTSes have labels on transitions, which can be viewed as a labelling function on transitions. Why is one simpler than the other? In the context of your question, using acronyms like "ACTL" is ambiguous because the "A" could mean *all paths* or *action-based*.

The difference, in my opinion, between Kripke structures and LTSes is based on modelling convenience and not simplicity. There is a lot of work comparing and contrasting the two. Here are a few starting points for chasing down related work.

1. De Nicola and Vaandrager have a few papers on translating between Kripke structures and LTSes and how this affects logical properties. They introduce doubly labelled transition systems to move between the two types of representations and semantic interpretations.

   [Action versus state based logics for transition systems](http://www.springerlink.com/content/y13110781p623363/) , De Nicola and Vaandrager, 1990

   [Three logics for branching bisimulation](http://portal.acm.org/citation.cfm?id=201032), De Nicola and Vaandrager, 1995
2. If the goal is verification of event-based systems, one option is to translate the LTS into a Kripke structure and use a Kripke structure model checker. The translation has to preserve the interpretation of CTL over the LTS.

   [An action-based framework for veryfying logical and behavioural properties of concurrent systems](http://dx.doi.org/10.1016/0169-7552%2893%2990047-8), De Nicola, Fantesi, Gnesi, Ristori
3. Translating between representations involves a blowup. For the case of LTL, there are cases when this blowup can be avoided. Here is a recent paper on the topic.

   [State/event-based software model checking](http://www.springerlink.com/index/npvpeukpe5nt0gjx.pdf), Chaki, Clarke, Ouaknine, Sharygina, Sinha

> **Comments:**
> **username_0**: Thanks, and yes simpler is probably a bad adjective to attach, maybe I used it because I learned LTSs first so they seem more natural to me but objectively there is no reason why they are simpler. Thanks for the links they do seem to be what I'm looking for.  

---

