Labeled Transition Systems (TaMie face to face review)

["Moberg Dale" <dmoberg@axway.com>]

Labeled Transition Systems (closely related to Kripke models) are used in studying finite (or infinite) state processes, and made their way into discussions because temporal logics used in computational process verification, testing, and safety proofs can be seen as part of the modal logic family. Kripke models have been in use for some time within modal logic model theory.

 

At the meeting I suggested that rather than try to deal directly with all the various process languages used in BPM, we instead cast our discussion toward labeled transition systems, which must be embedded within the process languages and which can be extracted out of them to give simply a set of states S, a set of transition conditions L, a set of edges E contained in the product, S X S, and a set of labelings,  E X L. (There are a lot of other ways to write out the components but this will do.)

 

The idea then is that a model written in BPEL, WS-CDL, XPDL, BPMN 2, ebBP BPSS, and so on be connected to TaMie through the labeled transition system embedded in the notation for the model. Several constructions for doing this (XSLTs) exist at least for ebBP BPSS; I suspect the others could also be sketched without too much work. The main task is to arrive at one (or several) mappings to the states, and the transitions should then be readily apparent. The main difficulty is in finding a good way to create the labels, which are logically speaking predicates, which when suitable bound to execution trace events, become Boolean valued first order assertions.

 

If this approach is adopted, we can then investigate how to compile a labeled transition system into an ETSL script. In fact that might be a good way to tell that our ETSL script language has enough power to relate BPM models to the events on the “blackboard”.  Verification of the model will then become validation of the test assertions, which will amount to a binding of events from the execution trace to the predicates (open assertions) that label transitions.

 

Also, by using LTS as the type of common process model that ETSL scripts relate to for BPM verification purposes, we also have models that should be consumable in a number of formal tools. Some tools are then used for proofs (within some formal calculus, such as the mu-calculus or pi-calculus or, more generally, some higher order proof environment, where mathematical induction is supported). Other tools are used to find counterexamples (such as a specific model where deadlock, livelock or some other feature of interest occurs).

 

I mentioned one tool available for the Eclipse environment called LTSA. Here is the link I said I would post to the list for LTSA tools. I have gotten them to work, but Eclipse is such a moving target, I did not have a working copy to show at the F2F.

 

http://www.doc.ic.ac.uk/ltsa/

 

 

There are a number of powerful algorithms associated with LTSes called bisimulation algorithms. Intuitively, these algorithms are used to decide whether the events satisfying one model would satisfy the other, and vice versa. So bisimulation results define equivalence relations, and thereby partition the LTSes. There are weaker and stronger equivalences that can be useful in studying problems such as: are the LTS models for one BPM notation the same as for another BPM notation or are the models satisfying a set of implementations also models that satisfy a set of Requirements (at a higher level of abstraction).

 

I don’t think we need in our group to explore the proof or test vector aspects of LTS. But I think working out how an ETSL script of test cases can be derived from a LTS would immerse our work in a wider context that might give it greater interest.