Weak and Nested Class Memory Automata
Conrad Cotton-Barratt, Andrzej Murawski, Luke Ong

TL;DR
This paper introduces a restriction called weakness to Class Memory Automata (CMA), making the emptiness problem equivalent to Petri Net Coverability, and extends CMA to nested data with decidable emptiness under this restriction.
Contribution
It identifies the weakness restriction in CMA, establishes its computational properties, and extends CMA to nested data with decidability results.
Findings
Weak CMA emptiness is equivalent to Petri Net Coverability.
Deterministic weak CMA are closed under all Boolean operations.
Weakness constraint recovers decidability for nested data CMA.
Abstract
Automata over infinite alphabets have recently come to be studied extensively as potentially useful tools for solving problems in verification and database theory. One popular model of automata studied is the Class Memory Automata (CMA), for which the emptiness problem is equivalent to Petri Net Reachability. We identify a restriction - which we call weakness - of CMA, and show that their emptiness problem is equivalent to Petri Net Coverability. Further, we show that in the deterministic case they are closed under all Boolean operations. We clarify the connections between weak CMA and existing automata over data languages. We also extend CMA to operate over multiple levels of nested data values, and show that while these have undecidable emptiness in general, adding the weakness constraint recovers decidability of emptiness, via reduction to coverability in well-structured transition…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · Logic, programming, and type systems
