By November 16, 2011 1 Comments Read More →

Colored Automata in Declare

This post has 765 words. Reading it will take approximately 4 minutes.

GD Star Rating

I just finished the implementation of colored automata in Declare.  The formal foundation is described in

  • [PDF] [DOI] F. Maggi, M. Montali, M. Westergaard, and W. van der Aalst, “Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata,” in Business Process Management, 2011, pp. 132-147.
    author = {Maggi, Fabrizio and Montali, Marco and Westergaard, Michael and van der Aalst, Wil},
    affiliation = {Eindhoven University of Technology, The Netherlands},
    title = {Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata},
    booktitle = {Business Process Management},
    series = {Lecture Notes in Computer Science},
    editor = {Rinderle-Ma, Stefanie and Toumani, Farouk and Wolf, Karsten},
    publisher = {Springer Berlin / Heidelberg},
    isbn = {978-3-642-23058-5},
    keyword = {Computer Science},
    pages = {132-147},
    volume = {6896},
    url = {},
    doi = {10.1007/978-3-642-23059-2_13},
    note = {10.1007/978-3-642-23059-2_13},
    abstract = {Today’s information systems record real-time information about business processes. This enables the monitoring of business constraints at runtime. In this paper, we present a novel runtime verification framework based on linear temporal logic and colored automata. The framework continuously verifies compliance with respect to a predefined constraint model. Our approach is able to provide meaningful diagnostics even after a constraint is violated. This is important as in reality people and organizations will deviate and in many situations it is not desirable or even impossible to circumvent constraint violations. As demonstrated in this paper, there are several approaches to recover after the first constraint violation. Traditional approaches that simply check constraints are unable to recover after the first violation and still foresee (inevitable) future violations. The framework has been implemented in the process mining tool ProM.},
    year = {2011}

The idea is that normally we construct an automaton accepting only all valid executions.  Assume we look at the model:

The model says that “if you are bored, you should go to a concert” (the reponse constraint from Bored to the the Concerts), “you can never go to both a Britney and a Xtina concert” (the non-coexistence constraint between Britney and Xtina Concerts), and “only after going to a Britney Concert, can you be truly happy” (the precedence constraint from Britney Concert to True Happiness).

Normally, we would translate it to this automaton:

Click for a larger version.  States with a double outline are states where all constraints are satisfied and states (there’s only one) with a dashed outline are states where at least one constraint can never be satisfied.  To just enact the system, this is fine.  Sometimes we wish to provide more information, such as indicating that some constraints are not currently satisfied.  For this we annotate each state with the state of the individual constraints and obtain this automaton:

We use the first letter of the constraints (N = non-coexiststence between Britney and Xtina, P = precedence that happiness can only occur after a Britney concert, and R = response that after being bored we have to go to a concert).  A letter in upper-case means that the constraint is satisfied in the state.  If the letter is in parentheses it means that it is possible to execute tasks that makes the constraint violated again.  A letter in lower-case means that the constraint is currently not satisfied but it is possible to execute tasks to make it satisfied.

This automaton is excellent for enactment in a controlled environment as we have information about all constraints available in constant time.  If we cannot control the actions of the user, we can only provide diagnostics.  For this, we need to be able to continue after an error.  For this, we make the full automaton:

This automaton furthermore has states with fewer than 3 letters; letters that are absent are constraints that are never possible to satisfy again.  In the figure, most of these states are at the top.  We basically expand the state 3 from the previous figure to provide diagnostics as we continue execution.  In the above example, we see that if we execute “True Happiness” without first going to a Britney concert, we no longer can satisfy the precedence constraint.  If we continue the execution, we work our way towards a part where it is also no longer possible to satisfy the non-coexistence constraint, because we have been to both a Britney and a Xtina concert.  We also see that it is always possible to satisfy the response constraint (simply by going to a concert).

These automata are exported directly from the Declare Designer:

Declare currently doesn’t use the colored automaton internally.  This feature is available now from the Subversion repository and will be part for Declare 2.4.

Posted in: Uncategorized

1 Comment on "Colored Automata in Declare"

Trackback | Comments RSS Feed

Post a Comment