Streaming transducers for algorithmic verification of single-pass list-processing programs
From MaRDI portal
Publication:5408580
Abstract: We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data domain that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next input symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenating data-string variables and new symbols formed from data variables, while avoiding duplication. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over input/output data-strings, are in PSPACE. We identify a class of imperative and a class of functional programs, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative programs dynamically modify a singly-linked heap by changing next-pointers of heap-nodes and by adding new nodes. The main restriction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.
Recommendations
Cited in
(30)- Copyless cost-register automata: structure, expressiveness, and closure properties
- Better complexity bounds for cost register automata
- On bidirectional runtime enforcement
- Pattern eliminating transformations
- Better complexity bounds for cost register automata
- Foundations of Boolean stream runtime verification
- Regular Programming for Quantitative Properties of Data Streams
- On runtime enforcement via suppressions
- Non-deterministic transducer models of retransmission protocols over noisy channels
- Extended symbolic finite automata and transducers
- Streaming ranked-tree-to-string transducers
- Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
- On the Model Checking Problem for Some Extension of CTL*
- Semantic Foundations for Deterministic Dataflow and Stream Processing
- Copyful streaming string transducers
- Equivalence checking problem for finite state transducers over semigroups
- Simple linear string constraints
- String-to-string interpretations with polynomial-size output
- Streaming Property Testing of Visibly Pushdown Languages *
- Streamable regular transductions
- Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines
- On first-order runtime enforcement of branching-time properties
- Reasoning on data words over numeric domains
- Expressiveness of streaming string transducers
- Nondeterministic Streaming String Transducers
- Sequentiality of string-to-context transducers
- An automata-theoretic approach to the verification of distributed algorithms
- scientific article; zbMATH DE number 7561615 (Why is no real title available?)
- Regular Transformations of Data Words Through Origin Information
- Complexity of regular functions
This page was built for publication: Streaming transducers for algorithmic verification of single-pass list-processing programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408580)
