Extend regular expressions to multi-actions to match part of the multi-action

[jgroote]

Issue migrated from trac ticket # 752

component: lps2pbes | priority: minor

2010-06-29 14:20:19: [email protected] created the issue

---

If we are interested for the absence of an action 'a', one can write: [true.a]false*. If the action 'a' occurs as part of a multi-action the above formula will not detect the occurrence. Thereto, we like to propose a notation that can deal with parts of multi-actions. Preferably, this is achieved by using regular expressions, e.g.: [true. a|(true)]false**

[jgroote]

2010-06-29 22:34:03: @twillems commented

---

Our current syntax for the mu-calculus indeed aligns badly with the multi-action setting. I second a change in the syntax to fix this, but the proposed syntax change seems odd to me, as it mixes state formulae and action formulae.

I would propose changing only the syntax of the action formulae to the following (only in (keeping the state formulae as they are):

alpha ::= bool_expr | 'forall d:D.' alpha | '!'alpha | alpha '&&' alpha | a(e_1,...,e_n) | alpha'|'alpha

This would enable one to write 'a(1)|true', with the intended meaning that any multi-action 'a(1)', but also 'a(1)|a(2)', 'a(1)|a(1)', 'a(1)|send', etc., would match.

The semantics of alpha is largely in line with the already used semantics. I suggest the following semantics for the construct 'alpha|alpha', but feel a bit uncomfortable with the notation here:

|[alpha_1 | alpha_2]|epsilon = { a_1(e_1)|...|a_n(e_n) : a_1(e_1)|..|a_i(e_i) in |[alpha_1]|epsilon /\ a_{i+1}(e_i+1)|...|a_n(e_n) in |[alpha_2]|epsilon }

Note: a in |[ a|true ]|epsilon is achieved via the equivalence a= a|tau. Perhaps this may lead to issues in our tools?

[jgroote]

2017-05-04 14:55:45: @wiegerw