Spot issueshttps://gitlab.lrde.epita.fr/spot/spot/-/issues2020-05-07T00:14:56+02:00https://gitlab.lrde.epita.fr/spot/spot/-/issues/408partial (co-)Büchi realizability2020-05-07T00:14:56+02:00Alexandre Duret-Lutzpartial (co-)Büchi realizabilityTaking the same automaton as in #407, let's assume that the condition is not α="(Fin(0)|Fin(1)|Fin(2)) | Inf(3)" but some more complex formula that has α as a subformula. You may also imagine more colors used in the automaton and in the rest of the conditions.
We can still discover that α is Büchi-realizable and replace it with `Inf(x)`. That would work like partial-degeneralization, but for (co-)Büchi-realizability.Taking the same automaton as in #407, let's assume that the condition is not α="(Fin(0)|Fin(1)|Fin(2)) | Inf(3)" but some more complex formula that has α as a subformula. You may also imagine more colors used in the automaton and in the rest of the conditions.
We can still discover that α is Büchi-realizable and replace it with `Inf(x)`. That would work like partial-degeneralization, but for (co-)Büchi-realizability.https://gitlab.lrde.epita.fr/spot/spot/-/issues/389LTL->UVW2019-06-06T11:34:05+02:00Alexandre Duret-LutzLTL->UVWThe fragment is defined in http://motesy.cs.uni-bremen.de/pdfs/atva2018.pdf
Is our translation able to produce UVW? (via dualization probably).
Should we add the fragment and the translation?The fragment is defined in http://motesy.cs.uni-bremen.de/pdfs/atva2018.pdf
Is our translation able to produce UVW? (via dualization probably).
Should we add the fragment and the translation?https://gitlab.lrde.epita.fr/spot/spot/-/issues/342$rose & $fell2018-04-05T17:18:32+02:00Alexandre Duret-Lutz$rose & $fellIn SVA we can write:
- `$rose(a)` to mean "`a` is now `1`, but it was `0` in the previous step (if that step exists)".
- `$fell(a)` to mean "`a` is now `0`, but it was `1` in the previous step (if that step exists)".
- `$stable(a)` to mean "`a` has the same value in the previous step if that step exists"
If we had past operators, we would be able to write the first one `a & (Y(!a) | !Y(1))` and the other two similarly. But even without past operators, these seem to be something we could translate quite easily because they are only looking one step back.
For instance if during a translation one state is labeled by `$rose(a)` we know that all outgoing transitions match `a`, and all incoming transitions match `!a`.
Note: SVA can also combine these notations with clocks, and in this case looking one step back is not enough.In SVA we can write:
- `$rose(a)` to mean "`a` is now `1`, but it was `0` in the previous step (if that step exists)".
- `$fell(a)` to mean "`a` is now `0`, but it was `1` in the previous step (if that step exists)".
- `$stable(a)` to mean "`a` has the same value in the previous step if that step exists"
If we had past operators, we would be able to write the first one `a & (Y(!a) | !Y(1))` and the other two similarly. But even without past operators, these seem to be something we could translate quite easily because they are only looking one step back.
For instance if during a translation one state is labeled by `$rose(a)` we know that all outgoing transitions match `a`, and all incoming transitions match `!a`.
Note: SVA can also combine these notations with clocks, and in this case looking one step back is not enough.https://gitlab.lrde.epita.fr/spot/spot/-/issues/291generalize the BA-typeness check2021-01-08T14:18:39+01:00Alexandre Duret-Lutzgeneralize the BA-typeness checkThe `is_scc_tba_type()` internal function used by `tra_to_tba()` is currently specialized to Rabin acceptance.
However, the original paper [Krishnan et al., ISAAC'94] presents the check in a way that works regardless of the acceptance condition. Take an automaton A with arbitrary acceptance condition:
1. find the set of "final transitions" F, i.e., transitions that cannot be part of a rejecting cycle
2. check if A is still accepting after you have removed all final transitions F.
If A - F is not accepting anymore, then the input automaton is equivalent to a Büchi automaton with the same transition structure as A, but acceptance Inf(F).
The difficult point is the first one. Finding a rejecting cycle can be done by complementing the acceptance condition and looking for an accepting cycle, however we do not yet have that for arbitrary acceptance. (At the time of writing, the generic emptiness checks on the `adl/generic-ec` branch only return `true/false` answers, but it feels like it would not be too difficult to teach them to return an accepting cycle.)
The paper then goes on and points that a DRA is DBA-realizable iff it is DBA-type, and this does not hold for all acceptance conditions. However we still have that a BA-type automaton is clearly BA-realizable, so it still makes sense to try this algorithm before attempting some other conversion that add states. For instance the Streett-to-TGBA could be simplified on SCCs that are BA-type, and so would the default strategy of `remove_fin()`. Also the recurrence check based on `LTL->TGBA->DPA->DRA->is_DBA_type?` could skip the `DPA->DRA` step.
In the long run, we should probably aim to refine `remove_fin()` so that the different strategies can be applied at the SCC level instead of the entire automaton.The `is_scc_tba_type()` internal function used by `tra_to_tba()` is currently specialized to Rabin acceptance.
However, the original paper [Krishnan et al., ISAAC'94] presents the check in a way that works regardless of the acceptance condition. Take an automaton A with arbitrary acceptance condition:
1. find the set of "final transitions" F, i.e., transitions that cannot be part of a rejecting cycle
2. check if A is still accepting after you have removed all final transitions F.
If A - F is not accepting anymore, then the input automaton is equivalent to a Büchi automaton with the same transition structure as A, but acceptance Inf(F).
The difficult point is the first one. Finding a rejecting cycle can be done by complementing the acceptance condition and looking for an accepting cycle, however we do not yet have that for arbitrary acceptance. (At the time of writing, the generic emptiness checks on the `adl/generic-ec` branch only return `true/false` answers, but it feels like it would not be too difficult to teach them to return an accepting cycle.)
The paper then goes on and points that a DRA is DBA-realizable iff it is DBA-type, and this does not hold for all acceptance conditions. However we still have that a BA-type automaton is clearly BA-realizable, so it still makes sense to try this algorithm before attempting some other conversion that add states. For instance the Streett-to-TGBA could be simplified on SCCs that are BA-type, and so would the default strategy of `remove_fin()`. Also the recurrence check based on `LTL->TGBA->DPA->DRA->is_DBA_type?` could skip the `DPA->DRA` step.
In the long run, we should probably aim to refine `remove_fin()` so that the different strategies can be applied at the SCC level instead of the entire automaton.Florian RenkinFlorian Renkinhttps://gitlab.lrde.epita.fr/spot/spot/-/issues/229improve performance of language_map()2017-09-06T11:39:31+02:00Alexandre Duret-Lutzimprove performance of language_map()instead of making all possible equivalence checks, use the construct from the proof of Lemma 4.1 in [Minimisation of Deterministic Parity and Büchi Automata and Relative Minimisation of Deterministic Finite Automata](https://arxiv.org/pdf/1007.1333.pdf).instead of making all possible equivalence checks, use the construct from the proof of Lemma 4.1 in [Minimisation of Deterministic Parity and Büchi Automata and Relative Minimisation of Deterministic Finite Automata](https://arxiv.org/pdf/1007.1333.pdf).https://gitlab.lrde.epita.fr/spot/spot/-/issues/197Change emptiness_check interface2017-11-15T14:34:25+01:00Maximilien ColangeChange emptiness_check interfaceThe class should provide two methods is_empty() and accepting_run(), to be consistent with the method offered by twa.
This allows to optimize the algorithms when there is no need to compute an accepting run (e.g. couvreur on terminal automata).The class should provide two methods is_empty() and accepting_run(), to be consistent with the method offered by twa.
This allows to optimize the algorithms when there is no need to compute an accepting run (e.g. couvreur on terminal automata).Spot 3https://gitlab.lrde.epita.fr/spot/spot/-/issues/175investigate how ra_to_ba can be generalized2017-11-15T14:34:25+01:00Alexandre Duret-Lutzinvestigate how ra_to_ba can be generalizedCan we write `ra_to_ba()` for transition-based generalized Rabin automata? Generalizing the technique of Krishnan et al. (ISAAC'94)?
If that works, we can combine that with #174 and our determinization procedure to obtain a way to decide whether an automaton represents a recurrence property.Can we write `ra_to_ba()` for transition-based generalized Rabin automata? Generalizing the technique of Krishnan et al. (ISAAC'94)?
If that works, we can combine that with #174 and our determinization procedure to obtain a way to decide whether an automaton represents a recurrence property.https://gitlab.lrde.epita.fr/spot/spot/-/issues/167Implement Kurshan's "poorman's inclusion test"2017-11-15T14:34:25+01:00Alexandre Duret-LutzImplement Kurshan's "poorman's inclusion test"Cf. R.P. Kurshan, *Complementing Büchi Automata in Polynomia Time*, J. of Comp. and Sys. Sc.
The complementation of deterministic automata is already implemented: it corresponds to calling remove_fin() after complementing the acceptance condition. The paper discusses doing this for non-deterministic automata in order to test inclusion. This could be useful, especially in non-Büchi cases, where the determinization procedure will require a degeneralization first.Cf. R.P. Kurshan, *Complementing Büchi Automata in Polynomia Time*, J. of Comp. and Sys. Sc.
The complementation of deterministic automata is already implemented: it corresponds to calling remove_fin() after complementing the acceptance condition. The paper discusses doing this for non-deterministic automata in order to test inclusion. This could be useful, especially in non-Büchi cases, where the determinization procedure will require a degeneralization first.https://gitlab.lrde.epita.fr/spot/spot/-/issues/110investigate use of SAT-based synthezis of deterministic automata using non-de...2017-11-15T14:34:25+01:00Alexandre Duret-Lutzinvestigate use of SAT-based synthezis of deterministic automata using non-deterministic inputI believe the code should work as-is, provided we should lift the "deterministic input" restriction, and document that the number of states needed to synthesize a deterministic automaton from a nondeterministic maybe need to be greater.
This came up in an email conversation with Jan Strejček, who assumed the SAT stuff was accepting non-deterministic input.I believe the code should work as-is, provided we should lift the "deterministic input" restriction, and document that the number of states needed to synthesize a deterministic automaton from a nondeterministic maybe need to be greater.
This came up in an email conversation with Jan Strejček, who assumed the SAT stuff was accepting non-deterministic input.https://gitlab.lrde.epita.fr/spot/spot/-/issues/36study effect of degen-lcache on ba-simul2017-11-15T14:34:26+01:00Alexandre Duret-Lutzstudy effect of degen-lcache on ba-simul % ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 511
enabling `lcache` causes some transitions to be merged
% ltl2tgba --ba -x degen-lcache=1,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 499
but it hinders the BA simulation-based reductions
% ltl2tgba --ba -x degen-lcache=1,degen-reset=1,ba-simul=1 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
45 2032 183
% ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=1 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
45 2016 187
This suggest that either we could fine-tune `degen-lcache` to pick a
more suitable level when offered the choice (maybe take the "natural"
level when offered the choice), or we could devise a simulation-based
reduction that is tailored to degeneralized automata (where we know
that cloned states recognized the same languages).
% ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 511
enabling `lcache` causes some transitions to be merged
% ltl2tgba --ba -x degen-lcache=1,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 499
but it hinders the BA simulation-based reductions
% ltl2tgba --ba -x degen-lcache=1,degen-reset=1,ba-simul=1 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
45 2032 183
% ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=1 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
45 2016 187
This suggest that either we could fine-tune `degen-lcache` to pick a
more suitable level when offered the choice (maybe take the "natural"
level when offered the choice), or we could devise a simulation-based
reduction that is tailored to degeneralized automata (where we know
that cloned states recognized the same languages).
https://gitlab.lrde.epita.fr/spot/spot/-/issues/35better translation or simplification of GF(a & Fb)2017-11-15T14:34:26+01:00Alexandre Duret-Lutzbetter translation or simplification of GF(a & Fb)`G(F(a & Fb))` is equivalent to `G(Fa & Fb)`, yet I know of no translator that is able to translate the first as efficiently as the second.
It gets worse with `G(F(a & F(b & Fc)))` etc.
Look at the rewriting rules in the [LIO2ALBA paper](http://arxiv.org/abs/0911.2033).
It has `GF(a & Fb) = GFa & GFb` as well as `GF(a | Gb) = GFa | FGb` (to apply in the other direction).
`G(F(a & Fb))` is equivalent to `G(Fa & Fb)`, yet I know of no translator that is able to translate the first as efficiently as the second.
It gets worse with `G(F(a & F(b & Fc)))` etc.
Look at the rewriting rules in the [LIO2ALBA paper](http://arxiv.org/abs/0911.2033).
It has `GF(a & Fb) = GFa & GFb` as well as `GF(a | Gb) = GFa | FGb` (to apply in the other direction).
https://gitlab.lrde.epita.fr/spot/spot/-/issues/33add support for EQLTL2017-11-15T14:34:27+01:00Alexandre Duret-Lutzadd support for EQLTLRead [Stutter-Invariant Languages, ω-Automata, and Temporal-Logic](http://homepages.inf.ed.ac.uk/kousha/stut_eqltl_vac.ps).
A basic plan would be:
- [ ] Add an ∃ unary operator
- [ ] modify the LTL parser to accept ∃ only at the top-level.
- [ ] add a function `label_filter(tgba_digraph_ptr& aut, bdd vars)` that removes all variables in `vars` from the labels of `aut`.
- [ ] Adjust the translations. To translate `∃(a,b) f(a,b,c,d)`, first translate `f(a,b,c,d)`, and then apply `label_filter` to remove `a`, and `b`. (Note in Couvreur/FM, removing `a,b` could be done during the same pass that complements promises.)
- [ ] Implement Etessami's conversion from BA to EQLTL.
- [ ] Implement a conversion from TGBA to EQLTL.
A more general idea would be to allow ∃ at all level in the
formulas, during the translation, we have to apply `bdd_exist` on
the BDD-rewriting of any subformula of a ∃ operator.
Would it be correct to do the same with ∀ and `bdd_forall`? If that is true, that gives us a conceptually simple way to negate an automaton: translate it to EQLTL, negate it (giving an ∀-quantified LTL formula), and translate it back.
Read [Stutter-Invariant Languages, ω-Automata, and Temporal-Logic](http://homepages.inf.ed.ac.uk/kousha/stut_eqltl_vac.ps).
A basic plan would be:
- [ ] Add an ∃ unary operator
- [ ] modify the LTL parser to accept ∃ only at the top-level.
- [ ] add a function `label_filter(tgba_digraph_ptr& aut, bdd vars)` that removes all variables in `vars` from the labels of `aut`.
- [ ] Adjust the translations. To translate `∃(a,b) f(a,b,c,d)`, first translate `f(a,b,c,d)`, and then apply `label_filter` to remove `a`, and `b`. (Note in Couvreur/FM, removing `a,b` could be done during the same pass that complements promises.)
- [ ] Implement Etessami's conversion from BA to EQLTL.
- [ ] Implement a conversion from TGBA to EQLTL.
A more general idea would be to allow ∃ at all level in the
formulas, during the translation, we have to apply `bdd_exist` on
the BDD-rewriting of any subformula of a ∃ operator.
Would it be correct to do the same with ∀ and `bdd_forall`? If that is true, that gives us a conceptually simple way to negate an automaton: translate it to EQLTL, negate it (giving an ∀-quantified LTL formula), and translate it back.
https://gitlab.lrde.epita.fr/spot/spot/-/issues/31Converting a TGBA into a PSL formula2017-11-15T14:34:27+01:00Alexandre Duret-LutzConverting a TGBA into a PSL formula[The ForSpec Temporal Logic: A New Temporal Property-Specification Language](http://www.cs.rice.edu/~vardi/papers/tacas02.ps.gz) gives a conversion from Büchi automata to PSL.
Here is my reinterpretation of their theorem.
Any omega regular language can be converted into a finite union of
the form $L_1.L_2$ where $L_1$ is a regular language, and $L_2$ can
be described by a deterministic automaton. An expression `e` for $L_1$ can be computed easily using the classical state-elimination algorithm, so $L_1.L_2$ can be encoded by `{e}!<>->f` where `f` is a formula for $L_2$.
$L_2$ can be represented by disjunctions of the formulae of the form `{e1;e2[*]}! && {e1;e2[*]}[]=> {e2[*]}!` where `e1` is a word going to an accepting state, and `e2[*]` is the loop language of that state (i.e., the language of all words that will come back to this state).
Running this construction on the Büchi automaton we produce for `FGa` will give `{1*;a}<>-> ({a;a*}! & {a;a*}[]=>{a*}!)`. The negation of this formula, on translated to TGBA and reduced by simulation, will give exactly the TGBA we want for `GFa`.
The above algorithm works with Büchi automata as input. The
resulting formula would be translated to a TBA (i.e., a
transition-based non-generalized Büchi automaton) because in the
current PSL translation `<>->` and `{...}!` are all translated with
the same unique acceptance condition (this probably makes
complementation of Büchi automata via PSL uninteresting).
- Can we find a translation from TGBA to PSL that will work with transition-based generalized acceptance?
- Can we find a translation to PSL to relies on the `GF` operators instead pf `[]=>`? The idea is that these would add generalized conditions, so that we obtain a TGBA when translating the formula back automata.
[The ForSpec Temporal Logic: A New Temporal Property-Specification Language](http://www.cs.rice.edu/~vardi/papers/tacas02.ps.gz) gives a conversion from Büchi automata to PSL.
Here is my reinterpretation of their theorem.
Any omega regular language can be converted into a finite union of
the form $L_1.L_2$ where $L_1$ is a regular language, and $L_2$ can
be described by a deterministic automaton. An expression `e` for $L_1$ can be computed easily using the classical state-elimination algorithm, so $L_1.L_2$ can be encoded by `{e}!<>->f` where `f` is a formula for $L_2$.
$L_2$ can be represented by disjunctions of the formulae of the form `{e1;e2[*]}! && {e1;e2[*]}[]=> {e2[*]}!` where `e1` is a word going to an accepting state, and `e2[*]` is the loop language of that state (i.e., the language of all words that will come back to this state).
Running this construction on the Büchi automaton we produce for `FGa` will give `{1*;a}<>-> ({a;a*}! & {a;a*}[]=>{a*}!)`. The negation of this formula, on translated to TGBA and reduced by simulation, will give exactly the TGBA we want for `GFa`.
The above algorithm works with Büchi automata as input. The
resulting formula would be translated to a TBA (i.e., a
transition-based non-generalized Büchi automaton) because in the
current PSL translation `<>->` and `{...}!` are all translated with
the same unique acceptance condition (this probably makes
complementation of Büchi automata via PSL uninteresting).
- Can we find a translation from TGBA to PSL that will work with transition-based generalized acceptance?
- Can we find a translation to PSL to relies on the `GF` operators instead pf `[]=>`? The idea is that these would add generalized conditions, so that we obtain a TGBA when translating the formula back automata.
https://gitlab.lrde.epita.fr/spot/spot/-/issues/30Build TGTA from the LTL formula2017-11-15T14:34:27+01:00Alexandre Duret-LutzBuild TGTA from the LTL formulaAdjusting Couvreur's translation to produce TGTA directly seems doable.
Can it be done in a way that avoid duplicating the code completely?
Adjusting Couvreur's translation to produce TGTA directly seems doable.
Can it be done in a way that avoid duplicating the code completely?
https://gitlab.lrde.epita.fr/spot/spot/-/issues/21TBA→BA2017-11-15T14:34:27+01:00Alexandre Duret-LutzTBA→BAWe have an involved degeneralization procedure that does TGBA→BA. However in practice, many TGBA have a single acceptance set (i.e., they are TBA). I believe we could work on a more efficient procedure for the TBA→BA case, it might even include some optimisations that are easier to do using a single acceptance set.We have an involved degeneralization procedure that does TGBA→BA. However in practice, many TGBA have a single acceptance set (i.e., they are TBA). I believe we could work on a more efficient procedure for the TBA→BA case, it might even include some optimisations that are easier to do using a single acceptance set.https://gitlab.lrde.epita.fr/spot/spot/-/issues/20NuSMV output2017-11-15T14:34:27+01:00Alexandre Duret-LutzNuSMV outputCan we have a NuSMV printer for TGBA?Can we have a NuSMV printer for TGBA?https://gitlab.lrde.epita.fr/spot/spot/-/issues/11more LTL simplifications for GF formulas2017-11-15T14:34:27+01:00Alexandre Duret-Lutzmore LTL simplifications for GF formulas`(GF(a)&GF(b)) | (GF(c)&GF(d))` is equivalent to `(GF(a|c) & GF(a|d) & GF(b|c) & GF (b|d))`.
It's a bigger formula, but it can be translated into a one-state automaton.
> Jan Strejcek:
>> ADL:
>> we like to simplify `GFa | GFb` as
>> `GF(a|b)` because `GF(a|b)` is easily translated as a deterministic
>> automaton. In the same way, `(GFa & GFb) | (GFc & GFd)`, which is
>> currently translated as a non-deterministic automaton, could be
>> rewritten as `GF(a|c) & GF(a|d) & GF(b|c) & GF(b|d)` which will be
>> translated as a deterministic automaton. Can this kind of rewriting
>> be generalized?
>
> I think I can provide a (partial) answer. The only
> non-obvious rule we have to add is the following:
>
> for pure eventually formulae m1,m2 (roughly speaking, the formulae starting
> with F), the following
> equivalence holds: G m1 | G m2 <=> G (m1|m2)
>
> With this rule and the standard rules
>
> G f1 & G f2 <=> G (f1&f2)
> distributivity: (A&B) | (C&D) <=> (A|C) & (A|D) & (B|C) & (B|D)
> or simply A | (C&D) <=> (A|C) & (A|D) applied twice
> F f1 | F f2 <=> F (f1|f2)
>
> one can transform `(GFa & GFb) | (GFc & GFd)` into `G( F(a|c) & F(a|d) & F(b|c) & F(b|d))`,
> which is enough to get determinstic automaton. A more interesting
> question may be "How to detect the situation when such rules should be
> applied". This especially applies to the distributivity as all other rules
> simply replace two modalities with one, which has usually positive effect on
> the translation and therefore the rules should be applied by default. I can
> imagine that distributivity will be applied only with `--deter` option and
> only to propagate disjunction downwards the syntactic tree (as disjunction
> is often a source of nondeterminism).
> Jan:
>> ADL:
>> It isn't as straightforward as it seems. For instance
>> adding only the `G(e1)|G(e2) = G(e1|e2)` without distribution
>> can be a serious regression:
>>
>> `G(Fa & Fb) | G(Fc & Fd)`: 3 states
>> `G((Fa & Fb) | (Fc & Fd))`: 15 states
>> `G(F(a | c) & F(a | d) & F(b | c) & F(b | d))`: 1 state
>>
>> I think for this to work we have to guarantee that all pure
>> eventualities will be rewritten as F(something).
>
> I guess that you want to say that each pure eventuality formula can be
> rewritten into a conjunction of F(something) formulae. I'm afraid this
> doesn't hold. For example, `GFa R Fb` is a pure eventuality formula
> equivalent to `GFa | GFb`... Hmm, but there is no problem in this
> particular case. I have to think about it with a fresh mind.
`(GF(a)&GF(b)) | (GF(c)&GF(d))` is equivalent to `(GF(a|c) & GF(a|d) & GF(b|c) & GF (b|d))`.
It's a bigger formula, but it can be translated into a one-state automaton.
> Jan Strejcek:
>> ADL:
>> we like to simplify `GFa | GFb` as
>> `GF(a|b)` because `GF(a|b)` is easily translated as a deterministic
>> automaton. In the same way, `(GFa & GFb) | (GFc & GFd)`, which is
>> currently translated as a non-deterministic automaton, could be
>> rewritten as `GF(a|c) & GF(a|d) & GF(b|c) & GF(b|d)` which will be
>> translated as a deterministic automaton. Can this kind of rewriting
>> be generalized?
>
> I think I can provide a (partial) answer. The only
> non-obvious rule we have to add is the following:
>
> for pure eventually formulae m1,m2 (roughly speaking, the formulae starting
> with F), the following
> equivalence holds: G m1 | G m2 <=> G (m1|m2)
>
> With this rule and the standard rules
>
> G f1 & G f2 <=> G (f1&f2)
> distributivity: (A&B) | (C&D) <=> (A|C) & (A|D) & (B|C) & (B|D)
> or simply A | (C&D) <=> (A|C) & (A|D) applied twice
> F f1 | F f2 <=> F (f1|f2)
>
> one can transform `(GFa & GFb) | (GFc & GFd)` into `G( F(a|c) & F(a|d) & F(b|c) & F(b|d))`,
> which is enough to get determinstic automaton. A more interesting
> question may be "How to detect the situation when such rules should be
> applied". This especially applies to the distributivity as all other rules
> simply replace two modalities with one, which has usually positive effect on
> the translation and therefore the rules should be applied by default. I can
> imagine that distributivity will be applied only with `--deter` option and
> only to propagate disjunction downwards the syntactic tree (as disjunction
> is often a source of nondeterminism).
> Jan:
>> ADL:
>> It isn't as straightforward as it seems. For instance
>> adding only the `G(e1)|G(e2) = G(e1|e2)` without distribution
>> can be a serious regression:
>>
>> `G(Fa & Fb) | G(Fc & Fd)`: 3 states
>> `G((Fa & Fb) | (Fc & Fd))`: 15 states
>> `G(F(a | c) & F(a | d) & F(b | c) & F(b | d))`: 1 state
>>
>> I think for this to work we have to guarantee that all pure
>> eventualities will be rewritten as F(something).
>
> I guess that you want to say that each pure eventuality formula can be
> rewritten into a conjunction of F(something) formulae. I'm afraid this
> doesn't hold. For example, `GFa R Fb` is a pure eventuality formula
> equivalent to `GFa | GFb`... Hmm, but there is no problem in this
> particular case. I have to think about it with a fresh mind.
https://gitlab.lrde.epita.fr/spot/spot/-/issues/9new option for branching postponement2017-11-15T14:34:27+01:00Alexandre Duret-Lutznew option for branching postponementImplement branching postponement only for states labeled by recurrence formulae.
Implement branching postponement only for states labeled by recurrence formulae.
Alexandre Duret-LutzAlexandre Duret-Lutz