Skip to main content
1 of 2
meolic
  • 223
  • 3
  • 8

If your background is CTL interpreted over Kripke structures and you looks for something similar interpreted over LTSs, than ACTL could be interesting.

Back in 1990, R. De Nicola and F. Vaandrager introduced ACTL as an action-based CTL (Action versus state based logics for transition systems, Semantics of Systems of Concurrent Processes (1990), pp. 407-419). It has been further studied in 1993 (R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori: An Action-Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems, Computer Networks and ISDN Systems, Vol. 25, No. 7., pp. 761-778.) and more recently in 2008 (R. Meolic, T. Kapus, Z. Brezočnik: ACTLW - An Action-based Computation Tree Logic With Unless Operator, Information Sciences, 178 (6), pp. 1542-1557.)

Main idea of ACTL (not to be confused with a subset of CTL with the same acronym) is to have similar operators and similar algorithms for model checking as those for CTL. Moreover, operators are defined by fixed-point expressions analog to those used for CTL. The complexity (I am not sure about expresiveness) of ACTL is somewhere between HML and propositional modal μ-calculus.

meolic
  • 223
  • 3
  • 8