Pith. sign in

REVIEW 1 major objections 3 minor 56 references

Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory

T0 review · 1 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read For a modal mu-calculus over infinite data words, the monitorable least-fixed-point properties are exactly the guarded ones; in the full logic monitorability is undecidable.

desk verdict Strong monitorability characterization for data-carrying modal mu-calculus, but the advertised 'no decidable fragment' claim outruns the theorems. read the letter →

arxiv 2506.06172 v1 pith:2CXHW6NG submitted 2025-06-06 cs.LO cs.FL

Luca Aceto , Antonis Achilleos , Duncan Paul Attard , Léo Exibard , Adrian Francalanza , Anna Ingólfsdóttir , Karoliina Lehtinen This is my paper
classification cs.LOcs.FL MSC 03B4568Q60
keywords runtimeverificationmonitorabilitymodalmu-calculusdatawordsregisterautomataHennessy-Milnerlogicwithguardedquantificationundecidability
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Runtime verification checks whether a system satisfies a specification by watching its execution trace; this paper extends that question to data-carrying traces and a modal mu-calculus over an infinite data domain with equality as the only predicate. It proves a strict hierarchy among fragments of the logic: the formula class cHMLd can be monitored soundly and completely for satisfactions by synthesizing monitors equivalent to alternating register automata with existential guessing. In the fragment without greatest fixed points, a formula is monitorable exactly when it is equivalent to a guarded formula in minHMLd∀g, and every such formula can be monitored optimally. In the full logic with greatest fixed points, monitorability and effective monitorability are undecidable. The paper therefore establishes where data-aware runtime monitoring is possible and why beyond that boundary it cannot be automated.

What carries the argument

The central object is annotation semantics: a graph of formula, data-environment, and trace triples that witnesses satisfaction, with least-fixed-point consistency ruling out infinite unfolding. Monitors essentially compute finite annotations, and the guarded fragment minHMLd∀g uses guarded-branching annotations, where a universal quantifier is evaluated by a finite set of explicit data values plus a dummy value representing all others, giving finite witnesses. The translation gd rewrites any least-fixed-point formula into guarded form, and the synthesis map from cHMLd formulae to monitors with guessing, parallel OR/AND, and recursion is what connects the logic to register automata.

What would settle it

Take the formula built from a deterministic Turing machine in Lemma 26: if monitorability were decidable, running the decider on that formula would decide whether the machine halts on 0, so a single machine for which the decider and direct simulation disagree would refute Corollary 28.

Watch

Extended reading notes

Core claim

The paper's central discovery is a precise boundary for runtime monitorability in the linear-time modal mu-calculus over data words. On the positive side, the fragment cHMLd is soundly and satisfaction-completely monitorable by a compositional synthesis procedure, and the resulting monitor model coincides with alternating register automata with existential guessing. On the structural side, within minHMLd—the fragment without greatest fixed points—a formula is monitorable for satisfactions exactly when it is equivalent to a formula of the guarded fragment minHMLd∀g, in which every universal quantifier is bounded by a guard; the translation gd makes any least-fixed-point formula optimally monitorable. On the negative side, as soon as greatest fixed points are allowed, monitorability and effective monitorability for sHMLd and µHMLd are undecidable, so no decidable fragment can capture all monitorable properties of the full logic.

Load-bearing premise

The framework assumes the data domain is countably infinite with equality as its only predicate, and that monitors may non-deterministically guess arbitrary data values.

Editorial extensions

If this is right

  • Every cHMLd formula has an effective, sound, satisfaction-complete monitor, and dually every sHMLd formula can be monitored for violations.
  • The different monitor models—deterministic, match-based, nonexistential, and alternating—correspond to inequivalent classes of register automata, so the choice of monitor model changes which properties are monitorable.
  • In minHMLd, satisfaction-monitorable properties have good prefixes, and the guarded translation gd(φ) yields an optimal monitor for φ even when φ itself is not obviously guarded.
  • Monitorability and effective monitorability for sHMLd and µHMLd are undecidable, so no decidable fragment of the full logic can cover all monitorable properties.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If data is treated as ordered rather than merely equal-or-different, the paper's complete-monitorability result changes even at the recursion-free level, so the clean boundary is tied to equality-only data.
  • Because deterministic monitors are strictly weaker than nondeterministic or alternating ones, toolchains built on deterministic register automata cannot be made complete by determinization alone; they would need to allow alternation or guessing.
  • The guarded fragment provides a syntactic template: a least-fixed-point formula that cannot be rewritten into guarded form is evidence of unmonitorability, although undecidability precludes a fully automatic check.
  • Implementing the gd translation in a monitoring tool and comparing the synthesized monitors with the cHMLd monitors would be a concrete stress test of the theory.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 3 minor

Summary. The paper studies monitorability of a linear-time variant of the modal mu-calculus over data words over a countably infinite domain with equality only. It defines the logic µHMLd and several fragments, proves a complete-monitorability characterisation (HMLd), a sound and satisfaction-complete synthesis for cHMLd/sHMLd, an equivalence between the monitor model and alternating register automata with existential guessing, and a guarded fragment minHMLd∀g that is claimed to capture exactly the monitorable formulas in the least-fixed-point fragment. It also proves undecidability of monitorability for sHMLd and µHMLd and interprets this as ruling out any decidable fragment that captures all monitorable properties.

Significance. The technical core is substantial and mostly convincing. The annotation semantics (Section 2.4) and the guarded-branching annotations (Section 4.1) are nontrivial tools, and the proofs of Theorems 16, 17, 21 and 25 are detailed. The register-automaton correspondence is a useful bridge to existing automata theory, and the strict hierarchy among monitor models is a valuable contrast with the finite-alphabet case. The concrete reductions from Turing-machine behaviour to monitorability in Corollaries 27 and 28 are clear assets. However, the advertised impossibility of a decidable expressively complete fragment is not established by those reductions, and one expressiveness proof in the appendix is incomplete. The contributions are therefore conditionally significant: the formal characterisations appear sound, but the paper's headline interpretive claim needs repair.

major comments (1)
  1. [Section 4.2 / Corollary 28 and Abstract] The undecidability of the predicate 'φ is monitorable for satisfactions' does not imply that there is no decidable fragment of µHMLd that captures all monitorable properties up to equivalence. A decidable, sound fragment F with the property that every monitorable φ is equivalent to some ψ∈F is logically compatible with 'φ is monitorable' being undecidable, since deciding whether an arbitrary φ has an equivalent representative in F is a separate problem. The proof of Corollary 28 gives no reduction from the existence of such an F to a decision procedure for monitorability, nor a direct proof that the equivalence closure of any decidable sound fragment omits some monitorable µHMLd property. The abstract's 'no decidable fragment' and Section 4.2's 'impossibility of a decidable, maximal monitorable fragment' are therefore stronger than what is proved. Please either prove the stronger claim or weaken it (e.g., to 'monitorability is undecidable' or to a precisely defined non-existence of a decidable maximal fragment), and adjust the abstract accordingly.
minor comments (3)
  1. [Appendix A.4.1, Proposition 30] The proof is incomplete. It states that L' = {w ∈ Trc | there exist x,y ∈ D such that w ∈ (xx)*y^ω} separates LTL with freeze from µHMLd, but the final sentence ('awaiting for an analogue of Kamp's theorem for data languages') stops short of an argument. Please supply a proof or explicitly mark the separation as open or conjectural.
  2. [Section 2.2] The statement 'We assume wlog that every occurrence of each fixed-point variable is within the scope of a modal operator in its defining fixed-point formula' is used without proof. For the modal mu-calculus over infinite alphabets this transformation is not self-evident, and the annotation semantics in Section 2.4 appears to rely on it. Please provide a justification or a reference.
  3. [Section 4.2] The phrase 'decidable, maximal monitorable fragment' is not formally defined. Since the paper's strongest conclusion depends on this notion, a precise definition (maximal under inclusion? closed under equivalence? syntactic?) is needed.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the central monitorability characterizations are derived from independently defined semantic notions, and the paper's self-citations are not load-bearing.

full rationale

The paper's main claims—Theorem 13 (HMLd characterizes completely monitorable properties), Theorem 16 (cHMLd/sHMLd are satisfaction/violation-complete), Theorem 17 (equivalence with alternating register automata with existential guessing), Theorem 21 (finite guarded-branching annotations characterize satisfaction in minHMLd∀g), and Theorem 25 (monitorability in minHMLd coincides with equivalence to a guarded formula)—are all supported by proofs in the paper or appendix, not merely assumed. The guarded fragment minHMLd∀g is defined syntactically, and monitorability is defined independently via good prefixes and monitor acceptance; the theorem that the two coincide is derived through the gd translation and Propositions 66–69, which are real arguments rather than restatements of the definitions. The paper cites the authors' prior work for the finite-alphabet analogues and for the register-automata correspondence, but the present proofs are self-contained adaptations (e.g., Propositions 42, 58, 59), so these citations are not load-bearing. The skeptic's concern about the abstract's 'no decidable fragment' claim being stronger than Corollary 28 is a logical-gap/correctness issue, not a circularity: undecidability of a membership predicate does not by itself rule out a decidable set of representatives up to equivalence, but this does not make any theorem circular. No equation is shown to reduce to its own input, and no fitted parameter is renamed as a prediction. Hence the circularity score is minimal.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper defines no free parameters fitted to data. It introduces new syntactic fragments and annotation semantics, but these are definitions rather than postulated entities. The main new objects (cHMLd, minHMLd∀g, guarded-branching annotations) are mathematical constructs whose properties are proven; they do not have independent falsifiable handles outside the theory.

assumptions (5)
  • domain assumption The data domain D is countably infinite, has equality as its only predicate, and equality is decidable.
    Stated in Section 2.1. It is the basis for the logic semantics, the monitor model, and the register automata equivalence; richer domains (e.g., with order) change the results (Remark 14).
  • standard math Every occurrence of a fixed-point variable is within the scope of a modal operator (guardedness).
    Assumed without loss of generality in Section 2.2; standard for the modal mu-calculus.
  • standard math Knaster-Tarski fixed point theorem and the iterative characterization of least fixed points.
    Used to define fixed point semantics and in the proof of Proposition 6; cited to [22] and [55].
  • standard math Undecidability of the halting problem for deterministic Turing machines.
    Used in Theorems 3, 4, and Corollary 28.
  • standard math The type of a word (its equality pattern) is fully determined by its length and equality relations, and there are finitely many types per length.
    Used in Proposition 39 and the proof of Proposition 42; this is a basic fact about equality-only domains.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory." pith.science (2026). https://pith.science/paper/2CXHW6NG

@misc{pith2026250606172,
  author       = {Pith},
  title        = {Pith review of: Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2CXHW6NG}},
  note         = {Machine review of arXiv:2506.06172}
}
read the original abstract

Runtime verification, also known as runtime monitoring, consists of checking whether a system satisfies a given specification by observing the trace it produces during its execution. It is used as a lightweight verification technique to complement or substitute costlier methods such as model-checking. In the regular setting, Hennessy-Milner logic with recursion, a variant of the modal mu-calculus, provides a versatile formalism for expressing linear- and branching-time specifications of the control flow of the system. In this paper, we shift the focus from control to data and study the monitorability of an extension of this logic that allows one to express properties of the data flow. Data values are modelled as values from an infinite domain. They are stored using data variables and manipulated using predicates and first-order quantification. The resulting logic is closely related to register automata with guessing. This correspondence yields a monitor synthesis algorithm, and allows us to derive a strict monitorability hierarchy between the different fragments of the logic, in stark contrast to the regular setting. In particular, restricting to deterministic monitors strictly reduces the set of monitorable properties. Last, we exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic. We finally show that this is unavoidable because, in fact, there is no decidable fragment of the logic that captures all monitorable properties.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

56 extracted references · 34 canonical work pages

  1. [1]

    Complexity results for modal logic with recursion via translations and tableaux

    Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, and Anna Ingólfsdóttir. Complexity results for modal logic with recursion via translations and tableaux . Logical Methods in Computer Science , Volume 20, Issue 3 , August 2024. URL: https://lmcs.episciences.org/14031, https://doi.org/10.46298/lmcs-20(3:14)2024 doi:10.46298/lmcs-20(3:14)2024

    work page doi:10.46298/lmcs-20(3:14)2024 2024

  2. [2]

    A monitoring tool for linear-time \( \) HML

    Luca Aceto, Antonis Achilleos, Duncan Paul Attard, L \' e o Exibard, Adrian Francalanza, and Anna Ing \' o lfsd \' o ttir. A monitoring tool for linear-time \( \) HML . Sci. Comput. Program. , 232:103031, 2024. URL: https://doi.org/10.1016/j.scico.2023.103031, https://doi.org/10.1016/J.SCICO.2023.103031 doi:10.1016/J.SCICO.2023.103031

    arXiv 2024

  3. [3]

    Determinizing monitors for HML with recursion

    Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ing \' o lfsd \' o ttir, and S var \" O rn Kjartansson. Determinizing monitors for HML with recursion. J. Log. Algebraic Methods Program. , 111:100515, 2020. URL: https://doi.org/10.1016/j.jlamp.2019.100515, https://doi.org/10.1016/J.JLAMP.2019.100515 doi:10.1016/J.JLAMP.2019.100515

    work page arXiv 2020

  4. [4]

    Adventures in monitorability: from branching to linear time and back again

    Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ing \' o lfsd \' o ttir, and Karoliina Lehtinen. Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. , 3( POPL ):52:1--52:29, 2019. https://doi.org/10.1145/3290365 doi:10.1145/3290365

    doi:10.1145/3290365 2019

  5. [5]

    The best a monitor can do

    Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ing \' o lfsd \' o ttir, and Karoliina Lehtinen. The best a monitor can do. In Christel Baier and Jean Goubault - Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference) , volume 183 of LIPIcs , pages 7:1--7:23....

    work page doi:10.4230/lipics.csl.2021.7 2021

  6. [6]

    O n R untime E nforcement via S uppressions

    Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ing \' o lfsd \' o ttir. O n R untime E nforcement via S uppressions. In CONCUR , volume 118 of LIPIcs , pages 34:1--34:17, 2018

    work page 2018

  7. [7]

    Hendren, Sascha Kuzins, Ondrej Lhot \' a k, Oege de Moor, Damien Sereni, Ganesh Sittampalam, and Julian Tibble

    Chris Allan, Pavel Avgustinov, Aske Simon Christensen, Laurie J. Hendren, Sascha Kuzins, Ondrej Lhot \' a k, Oege de Moor, Damien Sereni, Ganesh Sittampalam, and Julian Tibble. Adding trace matching with free variables to AspectJ . In Ralph E. Johnson and Richard P. Gabriel, editors, Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented...

    arXiv 2005

  8. [8]

    Schneider

    Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness. Distributed Comput. , 2(3):117--126, 1987. https://doi.org/10.1007/BF01782772 doi:10.1007/BF01782772

    doi:10.1007/bf01782772 1987

Show all 56 references
  1. [9]

    Apt and Gordon D

    Krzysztof R. Apt and Gordon D. Plotkin. Countable nondeterminism and random assignment. J. ACM , 33(4):724--767, 1986. https://doi.org/10.1145/6490.6494 doi:10.1145/6490.6494

    1986

  2. [10]

    Principles of Model Checking

    Christel Baier and Joost-Pieter Katoen. Principles of Model Checking . MIT Press, 2008

    2008

  3. [11]

    Rydeheard

    Howard Barringer, Yli \` e s Falcone, Klaus Havelund, Giles Reger, and David E. Rydeheard. Quantified event automata: Towards expressive and efficient runtime monitors. In Dimitra Giannakopoulou and Dominique M \' e ry, editors, FM 2012: Formal Methods - 18th International Sym...

    2012 doi

  4. [12]

    Rule-based runtime verification

    Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen. Rule-based runtime verification. In Bernhard Steffen and Giorgio Levi, editors, Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13,...

    2004 doi

  5. [13]

    Rydeheard, and Klaus Havelund

    Howard Barringer, David E. Rydeheard, and Klaus Havelund. Rule systems for run-time monitoring: From Eagle to RuleR . In Oleg Sokolsky and Serdar Tasiran, editors, Runtime Verification, 7th International Workshop, RV 2007, Vancouver, Canada, March 13, 2007, Revised Selected Pa...

    2007 doi

  6. [14]

    I ntroduction to R untime V erification

    Ezio Bartocci, Yli \` e s Falcone, Adrian Francalanza, and Giles Reger. I ntroduction to R untime V erification. In Lectures on Runtime Verification: Introductory and Advanced Topics , volume 10457 of LNCS , pages 1--33. Springer, 2018

    2018

  7. [15]

    Basin, Felix Klaedtke, and Samuel M \" u ller

    David A. Basin, Felix Klaedtke, and Samuel M \" u ller. Policy monitoring in first-order temporal logic. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedi...

    2010 doi

  8. [16]

    From propositional to first-order monitoring

    Andreas Bauer, Jan - Christoph K \" u ster, and Gil Vegliach. From propositional to first-order monitoring. In Axel Legay and Saddek Bensalem, editors, Runtime Verification - 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings , volume 817...

    2013 doi

  9. [17]

    On notions of regularity for data languages

    Henrik Bj \" o rklund and Thomas Schwentick. On notions of regularity for data languages. Theor. Comput. Sci. , 411(4-5):702--715, 2010. https://doi.org/10.1016/j.tcs.2009.10.009 doi:10.1016/j.tcs.2009.10.009

    2010 doi

  10. [18]

    Slightly Infinite Sets

    Miko aj Boja \' n czyk. Slightly Infinite Sets . 2019. URL: https://www.mimuw.edu.pl/ bojan/paper/atom-book

    2019

  11. [19]

    Two-variable logic on data words

    Mikolaj Bojanczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log. , 12(4):27:1--27:26, 2011. https://doi.org/10.1145/1970398.1970403 doi:10.1145/1970398.1970403

    2011

  12. [20]

    Automata theory in nominal sets

    Miko aj Boja \' n czyk, Bartek Klin, and S awomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci. , 10(3), 2014. https://doi.org/10.2168/LMCS-10(3:4)2014 doi:10.2168/LMCS-10(3:4)2014

    2014 doi

  13. [21]

    Narayan Kumar

    Benedikt Bollig, Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar. Model checking languages of data words. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures , pages 391--405, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg

    2012

  14. [22]

    Bradfield and Colin Stirling

    Julian C. Bradfield and Colin Stirling. Modal mu-calculi. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic , volume 3 of Studies in logic and practical reasoning , pages 721--756. North-Holland, 2007. URL: https://doi.org/10.101...

    2007 doi

  15. [23]

    Parametric trace slicing and monitoring

    Feng Chen and Grigore Rosu. Parametric trace slicing and monitoring. In Stefan Kowalewski and Anna Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences o...

    2009 doi

  16. [24]

    Sjoerd Cranen, Jan Friso Groote, and Michel A. Reniers. A linear translation from CTL* to the first-order modal \( \) -calculus. Theor. Comput. Sci. , 412(28):3129--3139, 2011. URL: https://doi.org/10.1016/j.tcs.2011.02.034, https://doi.org/10.1016/J.TCS.2011.02.034 doi:10.101...

    2011 doi

  17. [25]

    CTL* and ECTL* as fragments of the modal -calculus

    Mads Dam. CTL* and ECTL* as fragments of the modal -calculus. Theoretical Computer Science , 126(1):77--96, 1994. URL: https://www.sciencedirect.com/science/article/pii/0304397594902690, https://doi.org/https://doi.org/10.1016/0304-3975(94)90269-0 doi:https://doi.org/10.1016/0...

    1994

  18. [26]

    Temporal logic, automata and classical theories

    Mads Dam. Temporal logic, automata and classical theories. In P roceedings of the 6th E uropean S ummer S chool in L ogic, L anguage and I nformation ( ESSLLI '94) , August 1994

    1994

  19. [27]

    Efficient monitoring of omega-languages

    Marcelo d'Amorim and Grigore Rosu. Efficient monitoring of omega-languages. In Kousha Etessami and Sriram K. Rajamani, editors, Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings , volume 3576 of Lecture ...

    2005 doi

  20. [28]

    In the maze of data languages

    Loris D'Antoni. In the maze of data languages. CoRR , abs/1208.5980, 2012. URL: http://arxiv.org/abs/1208.5980, http://arxiv.org/abs/1208.5980 arXiv:1208.5980

    2012 arXiv

  21. [29]

    Monitoring modulo theories

    Normann Decker, Martin Leucker, and Daniel Thoma. Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. , 18(2):205--225, 2016. URL: https://doi.org/10.1007/s10009-015-0380-3, https://doi.org/10.1007/S10009-015-0380-3 doi:10.1007/S10009-015-0380-3

    2016 doi

  22. [30]

    LTL with the freeze quantifier and register automata

    St \' e phane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. , 10(3):16:1--16:30, 2009. https://doi.org/10.1145/1507244.1507246 doi:10.1145/1507244.1507246

    2009

  23. [31]

    On the freeze quantifier in constraint LTL: decidability and complexity

    St \' e phane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput. , 205(1):2--24, 2007. https://doi.org/10.1016/j.ic.2006.08.003 doi:10.1016/j.ic.2006.08.003

    2007 doi

  24. [32]

    Seshia, and Hadas Kress - Gazit

    R \" u diger Ehlers, Sanjit A. Seshia, and Hadas Kress - Gazit. Synthesis with identifiers. In Kenneth L. McMillan and Xavier Rival, editors, Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-2...

    2014 doi

  25. [33]

    Allen Emerson

    E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics , pages 995--1072. Elsevier and MIT Press, 1990. URL: https://doi.org/10.1016/b978-0-444-88074-1.50021-4

    1990 doi

  26. [34]

    Automatic Synthesis of Systems with Data

    L \'e o Exibard. Automatic Synthesis of Systems with Data . PhD Thesis , Aix-Marseille Universit \'e (AMU); Universit \'e libre de Bruxelles (ULB) , September 2021. URL: http://www.icetcs.ru.is/leoe/files/Exibard_ASSD_SASD.pdf

    2021

  27. [35]

    Synthesis of data word transducers

    L \' e o Exibard, Emmanuel Filiot, and Pierre - Alain Reynier. Synthesis of data word transducers. Logical Methods in Computer Science , 17(1), 2021. URL: https://lmcs.episciences.org/7279

    2021

  28. [36]

    A taxonomy for classifying runtime verification tools

    Yli \` e s Falcone, Srdan Krstic, Giles Reger, and Dmitriy Traytel. A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. , 23(2):255--284, 2021. URL: https://doi.org/10.1007/s10009-021-00609-z, https://doi.org/10.1007/S10009-021-00609-Z ...

    2021 doi

  29. [37]

    Reasoning on words and trees with data

    Diego Figueira. Reasoning on words and trees with data. ( Raisonnement sur mots et arbres avec donn \' e es) . PhD thesis, \' E cole normale sup \' e rieure de Cachan, France, 2010. URL: https://tel.archives-ouvertes.fr/tel-00718605

    2010

  30. [38]

    Alternating register automata on finite words and trees

    Diego Figueira. Alternating register automata on finite words and trees. Log. Methods Comput. Sci. , 8(1), 2012. https://doi.org/10.2168/LMCS-8(1:22)2012 doi:10.2168/LMCS-8(1:22)2012

    2012 doi

  31. [39]

    Relating timed and register automata

    Diego Figueira, Piotr Hofman, and Slawomir Lasota. Relating timed and register automata. Math. Struct. Comput. Sci. , 26(6):993--1021, 2016. https://doi.org/10.1017/S0960129514000322 doi:10.1017/S0960129514000322

    2016 doi

  32. [40]

    Diego Figueira, Anirban Majumdar, and M. Praveen. Playing with repetitions in data words using energy games. Log. Methods Comput. Sci. , 16(3), 2020. URL: https://lmcs.episciences.org/6614

    2020

  33. [41]

    Temporal stream logic: Synthesis beyond the bools

    Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. Temporal stream logic: Synthesis beyond the bools. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, P...

    2019 doi

  34. [42]

    Runtime verification based on register automata

    Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, and Nikos Tzevelekos. Runtime verification based on register automata. In Nir Piterman and Scott A. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TAC...

    2013

  35. [43]

    Verification of temporal properties of processes in a setting with data

    Jan Friso Groote and Radu Mateescu. Verification of temporal properties of processes in a setting with data. In Armando Martin Haeberer, editor, Algebraic Methodology and Software Technology, 7th International Conference, AMAST '98, Amazonia, Brasil, January 4-8, 1999, Proceed...

    1999 doi

  36. [44]

    Monitoring events that carry data

    Klaus Havelund, Giles Reger, Daniel Thoma, and Eugen Zalinescu. Monitoring events that carry data. In Ezio Bartocci and Yli \` e s Falcone, editors, Lectures on Runtime Verification - Introductory and Advanced Topics , volume 10457 of Lecture Notes in Computer Science , pages ...

    2018 doi

  37. [45]

    Finite-memory automata

    KF94 Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci. , 134(2):329--363, 1994. https://doi.org/10.1016/0304-3975(94)90242-9 doi:10.1016/0304-3975(94)90242-9

    1994 doi

  38. [46]

    Alternation-free modal mu-calculus for data trees

    Marcin Jurdzinski and Ranko Lazic. Alternation-free modal mu-calculus for data trees. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings , pages 131--140. IEEE Computer Society, 2007. https://doi.org/10.1109/LICS.2007...

    2007 doi

  39. [47]

    Finite-memory automata with non-deterministic reassignment

    Michael Kaminski and Daniel Zeitlin. Finite-memory automata with non-deterministic reassignment. Int. J. Found. Comput. Sci. , 21(5):741--760, 2010. https://doi.org/10.1142/S0129054110007532 doi:10.1142/S0129054110007532

    2010 doi

  40. [48]

    An overview of the MOP runtime verification framework

    Patrick O'Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen, and Grigore Rosu. An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. , 14(3):249--289, 2012. URL: https://doi.org/10.1007/s10009-011-0198-6, https://doi.org/10.1007/S100...

    2012 doi

  41. [49]

    Is computing an experimental science? J

    Robin Milner. Is computing an experimental science? J. Inf. Technol. , 2(2):58--66, 1987. URL: https://doi.org/10.1057/jit.1987.12, https://doi.org/10.1057/JIT.1987.12 doi:10.1057/JIT.1987.12

    1987 doi

  42. [50]

    Finite state machines for strings over infinite alphabets

    Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. , 5(3):403--435, 2004. https://doi.org/10.1145/1013560.1013562 doi:10.1145/1013560.1013562

    2004

  43. [51]

    Jean - \' E ric Pin. How to prove that a language is regular or star-free? In Alberto Leporati, Carlos Mart \' n - Vide, Dana Shapira, and Claudio Zandron, editors, Language and Automata Theory and Applications - 14th International Conference, LATA 2020, Milan, Italy, March 4-...

    2020 doi

  44. [52]

    Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science . Cambridge University Press, May 2013. URL: http://dx.doi.org/10.1017/CBO9781139084673, https://doi.org/10.1017/cbo9781139084673 doi:10.1017/cbo9781139084673

    2013 doi

  45. [53]

    Automata and logics for words and trees over an infinite alphabet

    Luc Segoufin. Automata and logics for words and trees over an infinite alphabet. In Zolt \' a n \' E sik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings , volume 42...

    2006 doi

  46. [54]

    Streett and E

    Robert S. Streett and E. Allen Emerson. An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation , 81(3):249--264, 1989. URL: https://doi.org/10.1016/0890-5401(89)90031-X

    1989 doi

  47. [55]

    A lattice-theoretical fixpoint theorem and its applications

    Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics , 5(2):285 -- 309, 1955. URL: https://doi.org/, https://doi.org/pjm/1103044538 doi:pjm/1103044538

    1955

  48. [56]

    Moshe Y. Vardi. A temporal fixpoint calculus. In Jeanne Ferrante and Peter Mager, editors, Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988 , pages 250--259. ACM Press, 1988. https:/...

    1988

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.