Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Lang, Frederic
We showed in a recent paper that, when verifying a modal $\mu$-calculus formula, the actions of the system under verification can be partitioned into sets of so-called weak and strong actions, depending on the combination of weak and strong modalities occurring in the formula. In a compositional verification setting, where the system consists of processes executing in parallel, this partition allows us to decide whether each individual process can be minimized for either divergence-preserving branching (if the process contains only weak actions) or strong (otherwise) bisimilarity, while preserving the truth value of the formula. In this paper, we refine this idea by devising a family of bisimilarity relations, named sharp bisimilarities, parameterized by the set of strong actions. We show that these relations have all the nice properties necessary to be used for compositional verification, in particular congruence and adequacy with the logic. We also illustrate their practical utility on several examples and case-studies, and report about our success in the RERS 2019 model checking challenge.
 I am Frédéric Long from Inria-Gronable. This talk is co-authored with Radou Matissekou from Inria-Gronable and Franco Masanti from CNR PISA. This talk deals with the verification of systems consisting of processes that run in parallel. The model of concurrency inherits from process algebra where parallel processes are represented by labeled transition systems. That is, automata whose edges are labeled by the system's communication actions. Those actions are executed asynchronously, meaning that from an observer point of view, independent concurrent actions interleave. There are operators enabling actions to be synchronized, renamed, or hidden. That is, renamed into a special internal action written tau. The properties to be verified on the system are expressed in the action-based model mu calculus, L mu, which is an expressive temporal logic that subsumes CTL, ACTL, PDL, and so on. Of course, verification has to tackle the famous state-space explosion problem. To do so, we rely on LTS reductions based on action-idling and bismillation, such as strong or deep branching bismillation. Strong bismillation allows those states which have exactly the same feature to be identified as equivalent without making any distinction in the treatment of internal and visible actions. Bismillation reduction consists in merging equivalent states, as in this example, where all equivalent states have been merged. Strong bismillation equivalence preserves all properties of L mu. Therefore, systems can always be reduced for strong bismillation. Deep branching bismillation is a shorthand for divergence preserving branching bismillation. It is a variant of the famous branching bismillation, which additionally preserves the cycles of tau transitions. Deep branching bismillation allows the source and target states of tau transitions to be considered as equivalent as long as they exhibit the same divergences and lead transitively to the same choices of visible actions. Deep branching bismillation reduction is illustrated in this example, where we can see that much more compression is obtained than with strong bismillation. When verifying a given temporal logic formula, we have to choose a reduction relation that preserves the formula. Based on this criterion, strong bismillation can always be chosen. To reduce the risk of explosion, deep branching should be favored as much as possible. With the same fragment of L mu called L mu dB was identified, which is preserved by deep branching. This fragment resembles L mu, but the modalities of L mu are replaced by restricted versions called weak modalities. This fragment subsumes other well-known logic fragments, such as CTL and ACTL, without next operator. Therefore, if we can prove that the formula can be expressed in L mu dB, then we can reduce the system for deep branching bismillation. However, if this is not the case, we have to resort to strong bismillation. In fact, we will see that we can do better. The fragment L mu dB preserved by deep branching bismillation offers three weak modalities written in PDL style. Note that we have to distinguish here between action predicates that are satisfied by the internal action tau and which are written alpha tau and action predicates that are not satisfied by tau and which are written alpha a. The first modality is called ultra weak modality. It expresses that there exists a finite sequence of actions satisfying alpha tau, which traverses only states satisfying the formula phi 1 and n in a state that satisfies the formula phi 2. The second modality is called weak modality. It differs from ultra weak modality, only in that the sequence ends in a state in which there is an action satisfying alpha a and leading to a state satisfying phi 2. The third modality is called weak infinite loop modality. It expresses that there exists an infinite sequence of actions satisfying alpha tau, which traverses only states satisfying the formula phi 1. Note that as soon as a formula contains a modality that cannot be expressed in a weak form, then deep branching reduction cannot be used because it may not preserve the truth value of the formula. From now, modalities that are not expressed in a weak form are called strong modalities. There are interesting properties that combine weak and strong modalities, such as searching for the occurrence of two consecutive actions or of a choice between actions after traversing an arbitrary sequence of possibly internal actions. In these examples, we can see that these formulas can be represented in a form where only a subset of the actions satisfy action predicates contained in strong modalities. We will see that this can be exploited to refine reduction with the new notion of sharp bisymbulation. From now, we assume that phi is represented in a form that combines weak and strong modalities. This form induces a partitioning of the system actions between those satisfied by the action formulas occurring in strong modalities, which we call strong actions, and the others, which we call weak. Sharp bisymbulation is parameterized by the set of strong actions. We show here its definition for those who already know the definitions of strong and deep branching bisymbulations. You can see here that sharp bisymbulation actually combines those definitions by distinguishing how weak and strong actions are treated. In particular, under some conditions, the transition labeled by a weak action can be matched by a sequence of tau transitions followed by the same weak action as in deep branching bisymbulation. Whereas this is not allowed for strong actions. If we now look back to our previous example, we can see that sharp reduction here, considering A as the only strong action, merges much more states than strong reduction, and almost as many as deep branching bisymbulation. This is a real progress as formulas which have only A as strong action can now be checked on an LTS with three states and three transitions instead of the strongly reduced LTS, which here has twice as many states and transitions. Remember that such formulas cannot be checked on the deep branching reduced LTS since they are not preserved by deep branching. Sharp bisymbulation has nice properties, which we have formally proven. These properties are not surprising, but they are useful and generalize non-properties of strong and deep branching bisymbulations. First, sharp bisymbulation with respect to set of strong actions, A as, is adequate with the fragment of L mu consisting of the formulas with strong modalities match on the actions in A as. Adequacy here means that the equivalent processes are those satisfying exactly the same formulas of the logic fragment. Second, of course, strong and deep branching are no instances of sharp bisymbulation. For strong bisymbulation, the set of strong actions is the universe of actions, including tau. For deep branching bisymbulation, the set of strong actions is empty. Moreover, the parameterization with respect to a set of strong actions defines a lattice of bisymulation relations. Third, the less actions are strong, the better the reduction is potentially. Finally, sharp bisymbularity is a congruence for parallel composition and hiding, which allows sharp reduction to be applied compositionally to processes and intermediate compositions. We applied sharp bisymbulation reduction in several contexts. The first one was the rarest challenge in 2019. We participated in the category consisting in verifying CTL properties and concurrent systems. In this category, 180 CTL properties had to be checked on nine different systems of increasing size. We used the CADP toolbox developed at INRIA to tackle these problems, and in particular, its compositional verification tools. Most of the properties were not preserved by deep branching. So we first tried compositional strong reduction, but this was not sufficient to palliate state space explosion for medium-sized problems. This is where the idea of sharp reduction arises. It turned out to be extremely successful, allowing all properties to be checked in only five rows on a standard laptop. We want all possible gold medals in this category. To give you an idea of the gain obtained using sharp reduction instead of strong reduction, I will only take a single example. This property of the challenge is not preserved by deep branching bisymbulation, as it contains strong actions, namely A8, A34, A57, and A60. Note that the other actions can be hidden in the system without changing the truth value of the property, and also that apart from the strong modalities that can be seen in this formula, it also has hidden weak modalities, encoding the CTL operators always finally and always weak until. The system on which this property was checked had 54 million states when unregistered. When using compositional strong reduction, the size of the largest LTS that had to be generated was about 10 times smaller. But when using compositional sharp reduction, the state space reduction was dramatic, leading to a largest LTS having only 200 states. We also applied sharp reduction into other contexts. First, we reviewed some experiments done initially in 2009 by Garavelle and Tyvol, using strong reduction at that time. The green line on top of the first diagram shows the number of states of the largest LTS generated using compositional strong reduction, whereas the red line concerns sharp reduction. The blue line concern or approach presented at FM-19 and can be here ignored. Note that the vertical axis is on the logarithmic scale. This diagram shows that the gain between strong and sharp bismillation is at least one order of magnitude. We also applied sharp reduction to example of the rarest 18 challenge. The diagram shows here that sharp reduction allowed us to solve problems that could not be tackled using strong bismillation. In this talk, we presented a new family of bismillation relations named sharp bismillations, which fills the gap between strong and deep branching bismillations. These relations are useful to verify formulas containing both strong and weak modalities, which in general do not enable deep branching reduction. The reduction in number of states may be dramatic as compared to strong bismillation and often close to the reduction obtained using deep branching. The experiments presented in this paper can be reproduced using CADP and the material made available in a Zenodo archive. Note that our tools only implement a partial sharp reduction, which is described in the paper. In the future, it will be nice to implement a full minimization algorithm. This is unfortunately not as simple as combining the algorithm for strong and deep branching bismillation minimization. There are issues related to cycles of tau transitions, which cannot be compressed beforehand, unlike what deep branching minimization algorithms do. Another point that should be improved is how to help the user extract weak and strong actions from the property. We already identified formula patterns in particular for CTL, but automated tools would be welcome. The smaller the set of strong actions, the better. However, for some formulas, there is no unique minimal set. In addition, we have shown that extracting a minimal set is at least as hard as testing the satisfiability of new calculus formula, which makes the automatic extraction of a minimal set of actions an x time hard problem. However, not necessarily minimal sets of strong actions can be useful. Finally, at first 19, we also used the sharp reduction approach in the context of LTL verification, with good results, as we also won all gold medals in this category. But this approach remains to be formalized. Thank you for your attention.
 I am Frédéric Long from Inria-Gronable.  This talk is co-authored with Radou Matissekou from Inria-Gronable  and Franco Masanti from CNR PISA.  This talk deals with the verification of systems consisting  of processes that run in parallel.  The model of concurrency inherits from process algebra  where parallel processes are represented  by labeled transition systems.  That is, automata whose edges are labeled  by the system's communication actions.  Those actions are executed asynchronously,  meaning that from an observer point of view,  independent concurrent actions interleave.  There are operators enabling actions  to be synchronized, renamed, or hidden.  That is, renamed into a special internal action written tau.  The properties to be verified on the system  are expressed in the action-based model mu calculus,  L mu, which is an expressive temporal logic  that subsumes CTL, ACTL, PDL, and so on.  Of course, verification has to tackle the famous state-space  explosion problem.  To do so, we rely on LTS reductions  based on action-idling and bismillation,  such as strong or deep branching bismillation.  Strong bismillation allows those states  which have exactly the same feature  to be identified as equivalent without making  any distinction in the treatment of internal and visible  actions.  Bismillation reduction consists in merging equivalent states,  as in this example, where all equivalent states have  been merged.  Strong bismillation equivalence preserves  all properties of L mu.  Therefore, systems can always be reduced  for strong bismillation.  Deep branching bismillation is a shorthand for divergence  preserving branching bismillation.  It is a variant of the famous branching bismillation, which  additionally preserves the cycles of tau transitions.  Deep branching bismillation allows the source and target  states of tau transitions to be considered as equivalent  as long as they exhibit the same divergences  and lead transitively to the same choices of visible actions.  Deep branching bismillation reduction  is illustrated in this example, where  we can see that much more compression is obtained  than with strong bismillation.  When verifying a given temporal logic formula,  we have to choose a reduction relation that  preserves the formula.  Based on this criterion, strong bismillation  can always be chosen.  To reduce the risk of explosion, deep branching  should be favored as much as possible.  With the same fragment of L mu called L mu dB  was identified, which is preserved by deep branching.  This fragment resembles L mu, but the modalities of L mu  are replaced by restricted versions called weak modalities.  This fragment subsumes other well-known logic fragments,  such as CTL and ACTL, without next operator.  Therefore, if we can prove that the formula can be expressed  in L mu dB, then we can reduce the system for deep branching  bismillation.  However, if this is not the case,  we have to resort to strong bismillation.  In fact, we will see that we can do better.  The fragment L mu dB preserved by deep branching bismillation  offers three weak modalities written in PDL style.  Note that we have to distinguish here  between action predicates that are satisfied  by the internal action tau and which are written alpha tau  and action predicates that are not satisfied by tau  and which are written alpha a.  The first modality is called ultra weak modality.  It expresses that there exists a finite sequence of actions  satisfying alpha tau, which traverses only states  satisfying the formula phi 1 and n in a state that  satisfies the formula phi 2.  The second modality is called weak modality.  It differs from ultra weak modality,  only in that the sequence ends in a state in which there  is an action satisfying alpha a and leading to a state  satisfying phi 2.  The third modality is called weak infinite loop modality.  It expresses that there exists an infinite sequence  of actions satisfying alpha tau, which traverses only states  satisfying the formula phi 1.  Note that as soon as a formula contains a modality that  cannot be expressed in a weak form,  then deep branching reduction cannot be used  because it may not preserve the truth value of the formula.  From now, modalities that are not expressed in a weak form  are called strong modalities.  There are interesting properties that combine weak and strong  modalities, such as searching for the occurrence  of two consecutive actions or of a choice between actions  after traversing an arbitrary sequence of possibly  internal actions.  In these examples, we can see that these formulas can  be represented in a form where only a subset of the actions  satisfy action predicates contained in strong modalities.  We will see that this can be exploited to refine reduction  with the new notion of sharp bisymbulation.  From now, we assume that phi is represented  in a form that combines weak and strong modalities.  This form induces a partitioning of the system actions  between those satisfied by the action formulas occurring  in strong modalities, which we call strong actions,  and the others, which we call weak.  Sharp bisymbulation is parameterized  by the set of strong actions.  We show here its definition for those who already  know the definitions of strong and deep branching bisymbulations.  You can see here that sharp bisymbulation actually  combines those definitions by distinguishing  how weak and strong actions are treated.  In particular, under some conditions,  the transition labeled by a weak action  can be matched by a sequence of tau transitions followed  by the same weak action as in deep branching bisymbulation.  Whereas this is not allowed for strong actions.  If we now look back to our previous example,  we can see that sharp reduction here,  considering A as the only strong action,  merges much more states than strong reduction,  and almost as many as deep branching bisymbulation.  This is a real progress as formulas which  have only A as strong action can now  be checked on an LTS with three states and three transitions  instead of the strongly reduced LTS, which here  has twice as many states and transitions.  Remember that such formulas cannot be checked  on the deep branching reduced LTS since they are not preserved  by deep branching.  Sharp bisymbulation has nice properties,  which we have formally proven.  These properties are not surprising,  but they are useful and generalize  non-properties of strong and deep branching bisymbulations.  First, sharp bisymbulation with respect  to set of strong actions, A as, is  adequate with the fragment of L mu consisting of the formulas  with strong modalities match on the actions in A as.  Adequacy here means that the equivalent processes  are those satisfying exactly the same formulas  of the logic fragment.  Second, of course, strong and deep branching  are no instances of sharp bisymbulation.  For strong bisymbulation, the set of strong actions  is the universe of actions, including tau.  For deep branching bisymbulation, the set of strong actions  is empty.  Moreover, the parameterization with respect  to a set of strong actions defines  a lattice of bisymulation relations.  Third, the less actions are strong,  the better the reduction is potentially.  Finally, sharp bisymbularity is a congruence  for parallel composition and hiding,  which allows sharp reduction to be applied compositionally  to processes and intermediate compositions.  We applied sharp bisymbulation reduction in several contexts.  The first one was the rarest challenge in 2019.  We participated in the category consisting  in verifying CTL properties and concurrent systems.  In this category, 180 CTL properties  had to be checked on nine different systems of increasing  size.  We used the CADP toolbox developed at INRIA  to tackle these problems, and in particular,  its compositional verification tools.  Most of the properties were not preserved by deep branching.  So we first tried compositional strong reduction,  but this was not sufficient to palliate state space explosion  for medium-sized problems.  This is where the idea of sharp reduction  arises.  It turned out to be extremely successful,  allowing all properties to be checked in only five  rows on a standard laptop.  We want all possible gold medals in this category.  To give you an idea of the gain obtained  using sharp reduction instead of strong reduction,  I will only take a single example.  This property of the challenge is not preserved  by deep branching bisymbulation, as it  contains strong actions, namely A8, A34, A57, and A60.  Note that the other actions can be hidden in the system  without changing the truth value of the property,  and also that apart from the strong modalities that  can be seen in this formula, it also  has hidden weak modalities, encoding the CTL operators  always finally and always weak until.  The system on which this property was checked  had 54 million states when unregistered.  When using compositional strong reduction,  the size of the largest LTS that had to be generated  was about 10 times smaller.  But when using compositional sharp reduction,  the state space reduction was dramatic,  leading to a largest LTS having only 200 states.  We also applied sharp reduction into other contexts.  First, we reviewed some experiments done initially  in 2009 by Garavelle and Tyvol, using strong reduction  at that time.  The green line on top of the first diagram  shows the number of states of the largest LTS  generated using compositional strong reduction,  whereas the red line concerns sharp reduction.  The blue line concern or approach presented at FM-19  and can be here ignored.  Note that the vertical axis is on the logarithmic scale.  This diagram shows that the gain between strong and sharp  bismillation is at least one order of magnitude.  We also applied sharp reduction to example  of the rarest 18 challenge.  The diagram shows here that sharp reduction  allowed us to solve problems that could not  be tackled using strong bismillation.  In this talk, we presented a new family of bismillation  relations named sharp bismillations,  which fills the gap between strong and deep branching  bismillations.  These relations are useful to verify formulas containing  both strong and weak modalities, which in general do not  enable deep branching reduction.  The reduction in number of states  may be dramatic as compared to strong bismillation  and often close to the reduction obtained  using deep branching.  The experiments presented in this paper  can be reproduced using CADP and the material made  available in a Zenodo archive.  Note that our tools only implement a partial sharp  reduction, which is described in the paper.  In the future, it will be nice to implement a full minimization  algorithm.  This is unfortunately not as simple  as combining the algorithm for strong and deep branching  bismillation minimization.  There are issues related to cycles of tau transitions,  which cannot be compressed beforehand,  unlike what deep branching minimization algorithms do.  Another point that should be improved  is how to help the user extract weak and strong actions  from the property.  We already identified formula patterns in particular for CTL,  but automated tools would be welcome.  The smaller the set of strong actions, the better.  However, for some formulas, there is no unique minimal set.  In addition, we have shown that extracting a minimal set  is at least as hard as testing the satisfiability of new calculus  formula, which makes the automatic extraction  of a minimal set of actions an x time hard problem.  However, not necessarily minimal sets of strong actions  can be useful.  Finally, at first 19, we also used the sharp reduction  approach in the context of LTL verification,  with good results, as we also won all gold medals  in this category.  But this approach remains to be formalized.  Thank you for your attention.
604907f51a80aac83ca25d7a_0_287.png 604907f51a80aac83ca25d7a_288_347.png 604907f51a80aac83ca25d7a_348_2279.png 604907f51a80aac83ca25d7a_2280_2351.png 604907f51a80aac83ca25d7a_2352_3035.png 604907f51a80aac83ca25d7a_3036_3083.png 604907f51a80aac83ca25d7a_3084_3239.png 604907f51a80aac83ca25d7a_3240_4379.png 604907f51a80aac83ca25d7a_4380_6011.png 604907f51a80aac83ca25d7a_6012_8099.png 604907f51a80aac83ca25d7a_8100_9635.png 604907f51a80aac83ca25d7a_9636_11351.png 604907f51a80aac83ca25d7a_11352_12587.png 604907f51a80aac83ca25d7a_12588_14783.png 604907f51a80aac83ca25d7a_14784_16559.png 604907f51a80aac83ca25d7a_16560_18503.png 604907f51a80aac83ca25d7a_18504_20087.png 604907f51a80aac83ca25d7a_20088_21143.png 604907f51a80aac83ca25d7a_21144_23747.png 604907f51a80aac83ca25d7a_23748_23819.png 604907f51a80aac83ca25d7a_23820_23867.png 604907f51a80aac83ca25d7a_23868_23885.png