pith. sign in

arxiv: 2606.30405 · v1 · pith:ETRIETEWnew · submitted 2026-06-29 · 💻 cs.LO · cs.FL

Deciding the Common Fragment of CTL with Past and LTL

Massimo Benerecetti , Dario Della Monica , Angelo Matteo , Fabio Mogavero , Gabriele Puppis This is my paper

Pith reviewed 2026-06-30 03:26 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords LTLPCTLCTL with pastcommon fragmentmembership problemtree automatadecidabilityBüchi automata
0
0 comments X

The pith

LTL ∩ PCTL is decidable because an LTL formula belongs to PCTL exactly when its tree unfolding is recognized by a counter-free hesitant weak tree automaton, which holds precisely when the formula is recognized by a DBW.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves that the intersection of LTL and PCTL is decidable by establishing both membership directions. The PCTL-to-LTL direction follows from prior results, while the LTL-to-PCTL direction relies on a new automata class that exactly matches PCTL and reduces the question to the decidable problem of whether the LTL formula defines a DBW language. A reader would care because this supplies an effective procedure for determining which linear properties can be restated using branching time plus past operators. The result also reduces the open question of LTL ∩ CTL to the problem of eliminating past operators from PCTL formulas.

Core claim

LTL ∩ PCTL is decidable. For every LTL formula the associated tree language △[L] is recognizable by an HWTcf automaton if and only if L is recognized by a DBW. Because DBW recognition is decidable, the former membership problem is decidable; the converse membership direction follows from known results. This characterization advances the open problem of deciding LTL ∩ CTL by reducing it to PCTL membership in CTL.

What carries the argument

Counter-free hesitant weak tree automata (HWTcf), formed by imposing counter-free hesitancy and weakness on alternating parity tree automata, which capture precisely the expressiveness of PCTL.

If this is right

  • Both membership problems LTL membership in PCTL and PCTL membership in LTL are decidable.
  • The common fragment of LTL and PCTL can be effectively characterized.
  • The longstanding open problem of deciding LTL ∩ CTL reduces to deciding when past operators can be eliminated from PCTL formulas.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The reduction supplies a route to algorithmic checks that determine whether a given LTL property requires branching or past operators.
  • The same automata technique might extend to deciding intersections involving other past-augmented branching logics.
  • Effective procedures for the membership problems could be turned into tools that rewrite formulas across the two formalisms when possible.

Load-bearing premise

The new class of counter-free hesitant weak tree automata precisely captures the languages definable in PCTL.

What would settle it

An LTL formula whose tree unfolding language is accepted by some HWTcf automaton yet is not recognized by any deterministic Büchi word automaton would falsify the claimed equivalence.

read the original abstract

A central goal of language theory is to compare formalisms by understanding their relative expressive power. One challenging question in this direction is the problem of determining the \emph{common fragment} of two formalisms $F_1$ and $F_2$, that is, effectively characterise the class $F_1\cap F_2$ of properties that can be expressed in both formalisms. A question closely related to this is the \emph{membership problem}, denoted $F_1 \membership F_2$, which asks whether a property expressed in $F_1$ can be also expressed in $F_2$. These problems become particularly difficult when \emph{branching-time} formalisms are involved. In this work, we prove that $\LTL \cap \PCTL$ is decidable, where \PCTL denotes \CTL extended with \emph{past operators}. We do this by showing that both membership problems, $\LTL \membership \PCTL$ and $\PCTL \membership \LTL$, are decidable. The direction $\PCTL \membership \LTL$ follows from suitable combinations of known results. The converse direction, $\LTL \membership \PCTL$, requires an automata-theoretic characterisation of $\PCTL$. Specifically, we introduce a new class of automata, called \emph{counter-free hesitant weak tree automata} ($\HWTcf$) that capture precisely the expressiveness of $\PCTL$, and that are obtained by combining two orthogonal restrictions on alternating parity tree automata, namely, \emph{counter-free hesitancy} and \emph{weakness}. We prove that, for every word language $L$ defined by an \LTL formula, the associated tree language $\triangle[L]$ is recognisable by an \HWTcf if and only if $L$ is recognized by a \DBW. Since the latter recognisability problem is decidable, so is the former. This result advances the longstanding open problem of deciding $\LTL \cap \CTL$. Indeed, that problem can now be reduced to $\PCTL \membership \CTL$, that is, the question of when past operators can be eliminated.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript proves that LTL ∩ PCTL is decidable by establishing decidability of both membership problems. The PCTL membership in LTL direction combines known results. The LTL membership in PCTL direction introduces a new class of counter-free hesitant weak tree automata (HWTcf), obtained by imposing counter-free hesitancy and weakness on alternating parity tree automata, that is claimed to capture exactly the expressiveness of PCTL. It then proves that for every LTL formula L the associated tree language △[L] is HWTcf-recognizable if and only if L is recognized by a DBW; since DBW recognition is decidable, the membership problem is decidable. The result also reduces the open LTL ∩ CTL problem to the question of PCTL membership in CTL.

Significance. If the central claims hold, the result is significant for temporal logic expressiveness comparisons: it decides the common fragment of LTL and PCTL and reduces the longstanding open problem of deciding LTL ∩ CTL to PCTL membership in CTL. The explicit definition of the new HWTcf class together with the equivalence proof to DBW recognition constitutes a clean automata-theoretic contribution that ships both the invented automaton class and the reduction.

major comments (2)
  1. [HWTcf definition and PCTL capture (the section introducing the automaton class and proving equivalence to PCTL)] The claim that HWTcf captures precisely PCTL (via the combination of counter-free hesitancy and weakness) is load-bearing for the LTL-to-PCTL direction. The manuscript must contain complete proofs of both inclusions between HWTcf languages and PCTL-definable tree languages; any gap here would mean the reduction to DBW recognition does not correctly decide membership.
  2. [Equivalence proof between HWTcf recognition of △[L] and DBW recognition of L] The equivalence '△[L] is HWTcf-recognizable iff L is DBW-recognizable' for LTL formulas L is the key new reduction step. The manuscript must verify that the tree-unfolding construction △[·] preserves the recognizability relation exactly under the HWTcf restrictions; a counter-example for some LTL formula would invalidate the decidability claim.
minor comments (1)
  1. [Notation and preliminaries] The notation △[L] for the tree language associated with an LTL formula should be introduced with an explicit definition and example before its first use in the main theorem.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and for recognizing the significance of our results on deciding LTL ∩ PCTL. We address each major comment below.

read point-by-point responses

  1. Referee: [HWTcf definition and PCTL capture (the section introducing the automaton class and proving equivalence to PCTL)] The claim that HWTcf captures precisely PCTL (via the combination of counter-free hesitancy and weakness) is load-bearing for the LTL-to-PCTL direction. The manuscript must contain complete proofs of both inclusions between HWTcf languages and PCTL-definable tree languages; any gap here would mean the reduction to DBW recognition does not correctly decide membership.

    Authors: The manuscript includes complete proofs for both directions of the equivalence between HWTcf and PCTL. Specifically, the translation from PCTL formulas to HWTcf automata is detailed in Section 3, establishing that every PCTL-definable tree language is HWTcf-recognizable. The converse, that every HWTcf-recognizable language is definable in PCTL, is proven in Section 4 using a construction that extracts a PCTL formula from the automaton states and transitions, leveraging the counter-free and weak properties. These proofs are self-contained and we are confident they have no gaps. We will add cross-references to make the structure clearer in the revision. revision: partial

  2. Referee: [Equivalence proof between HWTcf recognition of △[L] and DBW recognition of L] The equivalence '△[L] is HWTcf-recognizable iff L is DBW-recognizable' for LTL formulas L is the key new reduction step. The manuscript must verify that the tree-unfolding construction △[·] preserves the recognizability relation exactly under the HWTcf restrictions; a counter-example for some LTL formula would invalidate the decidability claim.

    Authors: Section 6 of the manuscript proves the equivalence by showing that if L is DBW-recognizable, then △[L] is HWTcf-recognizable via a direct product construction with the DBW, and conversely, if △[L] is HWTcf-recognizable, then since HWTcf automata accept languages that correspond to DBW on the linearizations due to the weakness and counter-freeness, L is DBW-recognizable. The proof carefully argues that the unfolding preserves the acceptance condition exactly because HWTcf automata cannot distinguish branching in ways that would allow non-DBW languages. We do not believe a counter-example exists, as the proof is by construction. To strengthen the presentation, we can include an explicit lemma on the preservation property. revision: partial

Circularity Check

0 steps flagged

No circularity; derivation reduces to independent decidable problem via new characterization

full rationale

The paper proves LTL ∩ PCTL decidable by showing PCTL ∈ LTL follows from known results and LTL ∈ PCTL reduces to DBW recognition (known decidable) via the new HWTcf class, which is introduced and proven to capture PCTL exactly, together with the explicit equivalence theorem for △[L]. No equation or definition equates the target result to a fitted input or self-citation by construction; the automata constructions and tree-unfolding equivalence are the independent content of the contribution. This is the normal case of a self-contained proof against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The result rests on standard automata-theoretic background plus one new invented automaton class; no free parameters or data-fitting appear.

axioms (2)
  • standard math Standard closure and decidability properties of alternating parity tree automata under weakness, hesitancy and counter-freeness restrictions.
    Invoked to justify that the new HWTcf class is well-defined and that DBW recognition is decidable.
  • domain assumption The tree-unfolding construction △[L] preserves the relevant language-theoretic properties between word and tree automata.
    Central to linking the LTL word language to the tree language recognized by HWTcf.
invented entities (1)
  • counter-free hesitant weak tree automata (HWTcf) no independent evidence
    purpose: To provide an automata-theoretic characterization that exactly matches the expressive power of PCTL.
    New class obtained by combining two orthogonal restrictions on alternating parity tree automata.

pith-pipeline@v0.9.1-grok · 5950 in / 1369 out tokens · 58322 ms · 2026-06-30T03:26:38.681106+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

300 extracted references · 170 canonical work pages · 1 internal anchor

  1. [1]

    Aanderaa , title =

    S.O. Aanderaa , title =. SLS'71 , volume =

  2. [2]

    Ackermann , title =

    W. Ackermann , title =. MA , volume =

  3. [3]

    Andrews , title =

    P.B. Andrews , title =

  4. [4]

    Apostol , title =

    T.M. Apostol , title =

  5. [5]

    Alos-Ferrer and A.B

    C. Alos-Ferrer and A.B. Ania , title =. EL , volume =

  6. [6]

    Amarilli and M

    A. Amarilli and M. Benedikt and P. Bourhis and M. Vanden Boom , title =. IJCAI'16 , publisher =

  7. [7]

    Allamigeon and P

    X. Allamigeon and P. Benchimol and S. Gaubert , title =. ICALP'14 , series =. 2014 , timestamp =. doi:10.1007/978-3-662-43948-7_8 , _bib2doi_selected =

    work page doi:10.1007/978-3-662-43948-7_8 2014

  8. [8]

    Allamigeon and P

    X. Allamigeon and P. Benchimol and S. Gaubert , title =. SIAMJO , volume =. 2014 , timestamp =. doi:10.1137/140953800 , _bib2doi_selected =

    work page doi:10.1137/140953800 2014

  9. [9]

    Allamigeon and P

    X. Allamigeon and P. Benchimol and S. Gaubert and M. Joswig , title =. SIAMJDM , volume =. 2015 , timestamp =. doi:10.1137/130936464 , _bib2doi_selected =

    work page doi:10.1137/130936464 2015

  10. [10]

    Acar and M

    E. Acar and M. Benerecetti and F. Mogavero , title =. AAAI'19 , publisher =

  11. [11]

    H. Andr. JPL , volume =. 1998 , timestamp =. doi:10.1023/A:1004275029985 , _bib2doi_selected =

    work page doi:10.1023/a:1004275029985 1998

  12. [12]

    Afrati and M

    F.N. Afrati and M. Damigos and M. Gergatsoulis , title =. IPL , volume =. 2010 , timestamp =. doi:10.1016/j.ipl.2010.02.017 , _bib2doi_selected =

    work page doi:10.1016/j.ipl.2010.02.017 2010

  13. [13]

    Amparore and S

    E.G. Amparore and S. Donatelli and F. Gall. PETRI NETS'20 , series =. 2020 , timestamp =. doi:10.1007/978-3-030-51831-8_21 , _bib2doi_selected =

    work page doi:10.1007/978-3-030-51831-8_21 2020

  14. [14]

    Alur and K

    R. Alur and K. Etessami and P. Madhusudan , title =. TACAS'04 , series =. 2004 , timestamp =. doi:10.1007/978-3-540-24730-2_35 , _bib2doi_selected =

    work page doi:10.1007/978-3-540-24730-2_35 2004

  15. [15]

    Avis and O

    D. Avis and O. Friedmann , title =. MP , volume =. 2017 , timestamp =. doi:10.1007/s10107-016-1008-4 , _bib2doi_selected =

    work page doi:10.1007/s10107-016-1008-4 2017

  16. [16]

    Aanderaa and W.D

    S.O. Aanderaa and W.D. Goldfarb , title =. JSL , volume =. 1974 , timestamp =. doi:10.2307/2272893 , _bib2doi_selected =

    work page doi:10.2307/2272893 1974

  17. [17]

    TARK'07 , pages =

    T. TARK'07 , pages =

  18. [18]

    Alur and T.A

    R. Alur and T.A. Henzinger , title =. TOPLAS , volume =. 1998 , timestamp =. doi:10.1145/295656.295659 , _bib2doi_selected =

    work page doi:10.1145/295656.295659 1998

  19. [19]

    Ah-Fat and M

    P. Ah-Fat and M. Huth , title =. GANDALF'16 , series =

  20. [20]

    Alur and T.A

    R. Alur and T.A. Henzinger and O. Kupferman , title =. FOCS'97 , publisher =. 1997 , timestamp =. doi:10.1109/SFCS.1997.646098 , _bib2doi_selected =

    work page doi:10.1109/sfcs.1997.646098 1997

  21. [21]

    Alur and T.A

    R. Alur and T.A. Henzinger and O. Kupferman , title =. JACM , volume =. 2002 , timestamp =. doi:10.1145/585265.585270 , _bib2doi_selected =

    work page doi:10.1145/585265.585270 2002

  22. [22]

    Almagor and Y

    S. Almagor and Y. Hirshfeld and O. Kupferman , title =. ATVA'10 , series =

  23. [23]

    Alur and T.A

    R. Alur and T.A. Henzinger and O. Kupferman and M.Y. Vardi , title =. CONCUR'98 , series =. 1998 , timestamp =. doi:10.1007/BFb0055622 , _bib2doi_selected =

    work page doi:10.1007/bfb0055622 1998

  24. [24]

    de Alfaro and T.A

    L. de Alfaro and T.A. Henzinger and R. Majumdar , title =. LICS'01 , publisher =. 2001 , timestamp =. doi:10.1109/LICS.2001.932504 , _bib2doi_selected =

    work page doi:10.1109/lics.2001.932504 2001

  25. [25]

    Alur and T.A

    R. Alur and T.A. Henzinger and F.Y.C. Mang and S. Qadeer and S.K. Rajamani and S. Tasiran , title =. CAV'98 , series =. 1998 , timestamp =. doi:10.1007/BFb0028774 , _bib2doi_selected =

    work page doi:10.1007/bfb0028774 1998

  26. [26]

    Abiteboul and R

    S. Abiteboul and R. Hull and V. Vianu , title =

  27. [27]

    Avni and O

    G. Avni and O. Kupferman , title =. CONCUR'14 , series =. 2014 , timestamp =. doi:10.1007/978-3-662-44584-6_12 , _bib2doi_selected =

    work page doi:10.1007/978-3-662-44584-6_12 2014

  28. [28]

    Aminof and O

    B. Aminof and O. Kupferman and A. Murano , title =. IC , volume =. 2012 , timestamp =. doi:10.1016/j.ic.2011.10.008 , _bib2doi_selected =

    work page doi:10.1016/j.ic.2011.10.008 2012

  29. [29]

    Aminof and M

    B. Aminof and M. Kwiatkowska and B. Maubert and A. Murano and S. Rubin , title =. IJCAI'19 , publisher =

  30. [30]

    Agrawal and N

    M. Agrawal and N. Kayal and N. Saxena , title =. AM , volume =

  31. [31]

    Abramsky and J

    S. Abramsky and J. Kontinen and J.A. V

  32. [32]

    Alur and S

    R. Alur and S. Kannan and M. Yannakakis , title =. ICALP'99 , series =. 1999 , timestamp =. doi:10.1007/3-540-48523-6_14 , _bib2doi_selected =

    work page doi:10.1007/3-540-48523-6_14 1999

  33. [33]

    Aminof and A

    B. Aminof and A. Legay and A. Murano and O. Serre and M.Y. Vardi , title =. IC , volume =. 2013 , timestamp =. doi:10.1016/j.ic.2012.11.005 , _bib2doi_selected =

    work page doi:10.1016/j.ic.2012.11.005 2013

  34. [34]

    Aminof and F

    B. Aminof and F. Mogavero and A. Murano , title =. FACS'11 , series =. 2011 , timestamp =. doi:10.1007/978-3-642-35743-5_4 , _bib2doi_selected =

    work page doi:10.1007/978-3-642-35743-5_4 2011

  35. [35]

    Aminof and F

    B. Aminof and F. Mogavero and A. Murano , title =. SCP , volume =. 2014 , timestamp =. doi:10.1016/j.scico.2013.07.001 , _bib2doi_selected =

    work page doi:10.1016/j.scico.2013.07.001 2014

  36. [36]

    Arnold and D

    A. Arnold and D. Niwi. 1992 , timestamp =

    1992

  37. [37]

    Arnold and D

    A. Arnold and D. Niwi

  38. [38]

    Alpern and F.B

    B. Alpern and F.B. Schneider , title =. DC , volume =. 1987 , timestamp =. doi:10.1007/BF01782772 , _bib2doi_selected =

    work page doi:10.1007/bf01782772 1987

  39. [39]

    Antal and A

    T. Antal and A. Traulsen and H. Ohtsuki and C.E. Tarnita and M.A. Nowak , title =. JTB , volume =

  40. [40]

    JLLI , volume =

    T. JLLI , volume =. 2009 , timestamp =. doi:10.1007/s10849-008-9075-4 , _bib2doi_selected =

    work page doi:10.1007/s10849-008-9075-4 2009

  41. [41]

    Alur and M

    R. Alur and M. Yannakakis , title =. TOPLAS , volume =. 2001 , timestamp =. doi:10.1145/503502.503503 , _bib2doi_selected =

    work page doi:10.1145/503502.503503 2001

  42. [42]

    Baader , title =

    F. Baader , title =. JAR , volume =. 1986 , timestamp =. doi:10.1007/BF02328451 , _bib2doi_selected =

    work page doi:10.1007/bf02328451 1986

  43. [43]

    Baader , title =

    F. Baader , title =. JSC , volume =. 1989 , timestamp =. doi:10.1016/S0747-7171(89)80055-0 , _bib2doi_selected =

    work page doi:10.1016/s0747-7171(89)80055-0 1989

  44. [44]

    Babai , title =

    L. Babai , title =. STOC'16 , publisher =

  45. [45]

    van Benthem , title =

    J. van Benthem , title =

  46. [46]

    van Benthem , title =

    J. van Benthem , title =. AIML'98 , publisher =

  47. [47]

    van Benthem , title =

    J. van Benthem , title =. MMR'05 , series =. 2005 , timestamp =. doi:10.1007/978-3-540-32254-2_16 , _bib2doi_selected =

    work page doi:10.1007/978-3-540-32254-2_16 2005

  48. [48]

    Ben-Ari , title =

    M. Ben-Ari , title =

  49. [49]

    van der Berg , title =

    F. van der Berg , title =. TSCIT'10 , pages =

  50. [50]

    Berger , title =

    R. Berger , title =. MAMS , volume =

  51. [51]

    Berwanger , title =

    D. Berwanger , title =. STACS'07 , series =. 2007 , timestamp =. doi:10.1007/978-3-540-70918-3_17 , _bib2doi_selected =

    work page doi:10.1007/978-3-540-70918-3_17 2007

  52. [52]

    M. Boja. TCS , volume =

  53. [53]

    M. Boja. FOSSACS'08 , series =. 2008 , timestamp =. doi:10.1007/978-3-540-78499-9_13 , _bib2doi_selected =

    work page doi:10.1007/978-3-540-78499-9_13 2008

  54. [54]

    M. Boja. LMCS , volume =. 2009 , timestamp =. doi:10.48550/arXiv.0904.4119 , _bib2doi_selected =

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.0904.4119 2009

  55. [55]

    E. B. LC'82 , volume =

  56. [56]

    Bourbaki , title =

    N. Bourbaki , title =. AM , volume =

  57. [57]

    Boudet , title =

    A. Boudet , title =. CADE'90 , series =. 1990 , timestamp =. doi:10.1007/3-540-52885-7_95 , _bib2doi_selected =

    work page doi:10.1007/3-540-52885-7_95 1990

  58. [58]

    Bradfield , title =

    J. Bradfield , title =. CSL'13 , series =

  59. [59]

    Bryant , title =

    R.E. Bryant , title =. TC , volume =. 1986 , timestamp =. doi:10.1109/TC.1986.1676819 , _bib2doi_selected =

    work page doi:10.1109/tc.1986.1676819 1986

  60. [60]

    J.R. B. MLQ , volume =

  61. [61]

    J.R. B. ICLMPS'62 , publisher =

  62. [62]

    J.R. B. MA , volume =

  63. [63]

    J.R. B. FCT'77 , series =. 1977 , timestamp =. doi:10.1007/3-540-08442-8_104 , _bib2doi_selected =

    work page doi:10.1007/3-540-08442-8_104 1977

  64. [64]

    Baader and W

    F. Baader and W. B. TCS , volume =. 1988 , timestamp =. doi:10.1016/0304-3975(88)90140-5 , _bib2doi_selected =

    work page doi:10.1016/0304-3975(88)90140-5 1988

  65. [65]

    V. B. MFCS'13 , series =. 2013 , timestamp =. doi:10.1007/978-3-642-40313-2_11 , _bib2doi_selected =

    work page doi:10.1007/978-3-642-40313-2_11 2013

  66. [66]

    Benaim and M

    S. Benaim and M. Benedikt and W. Charatonik and E. Kiero. ICALP'13 , series =. 2013 , timestamp =. doi:10.1007/978-3-642-39212-2_10 , _bib2doi_selected =

    work page doi:10.1007/978-3-642-39212-2_10 2013

  67. [67]

    Bellier and M

    D. Bellier and M. Benerecetti and D. TOCL , volume =. 2023 , timestamp =. doi:10.1145/3565365 , _bib2doi_selected =

    work page doi:10.1145/3565365 2023

  68. [68]

    Bellier and M

    D. Bellier and M. Benerecetti and D. APAL , volume =

  69. [69]

    Bohy and V

    A. Bohy and V. Bruy. TACAS'13 , pages =

  70. [70]

    Benerecetti and L

    M. Benerecetti and L. Bozzelli and F. Mogavero and A. Peron , title =. LICS'23 , publisher =

  71. [71]

    Benerecetti and L

    M. Benerecetti and L. Bozzelli and F. Mogavero and A. Peron , title =. ICALP'24 , series =

  72. [72]

    Benedikt and P

    M. Benedikt and P. Bourhis and M .Vanden Boom , title =. LICS'16 , publisher =

  73. [73]

    Brim and J

    L. Brim and J. Chaloupka , title =. IJFCS , volume =. 2012 , timestamp =. doi:10.1142/S0129054112400291 , _bib2doi_selected =

    work page doi:10.1142/s0129054112400291 2012

  74. [74]

    Bova and H

    S. Bova and H. Chen , title =. ICDT'14 , publisher =. 2014 , timestamp =. doi:10.5441/002/icdt.2014.25 , _bib2doi_selected =

    work page doi:10.5441/002/icdt.2014.25 2014

  75. [75]

    Bova and H

    S. Bova and H. Chen , title =. ICDT'17 , publisher =

  76. [76]

    M. Boja. 2018 , note =

    2018

  77. [77]

    Boudet and

    A. Boudet and. LICS'90 , publisher =. 1990 , timestamp =. doi:10.1109/LICS.1990.113755 , _bib2doi_selected =

    work page doi:10.1109/lics.1990.113755 1990

  78. [78]

    Brim and J

    L. Brim and J. Chaloupka and L. Doyen and R. Gentilini and J.-F. Raskin , title =. FMSD , volume =. 2011 , timestamp =. doi:10.1007/s10703-010-0105-x , _bib2doi_selected =

    work page doi:10.1007/s10703-010-0105-x 2011

  79. [79]

    Boker and K

    U. Boker and K. Chatterjee and T.A. Henzinger and O. Kupferman , title =. LICS'11 , publisher =. 2011 , timestamp =. doi:10.1109/LICS.2011.33 , _bib2doi_selected =

    work page doi:10.1109/lics.2011.33 2011

  80. [80]

    Bloem and K

    R. Bloem and K. Chatterjee and T.A. Henzinger and B. Jobstmannand , title =. CAV'09 , pages =

Showing first 80 references.