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)- Copyful streaming string transducers
- Simple linear string constraints
- Streaming ranked-tree-to-string transducers
- Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
- On bidirectional runtime enforcement
- Pattern eliminating transformations
- scientific article; zbMATH DE number 7561615 (Why is no real title available?)
- Foundations of Boolean stream runtime verification
- Complexity of regular functions
- On first-order runtime enforcement of branching-time properties
- Streamable regular transductions
- Nondeterministic Streaming String Transducers
- String-to-string interpretations with polynomial-size output
- Non-deterministic transducer models of retransmission protocols over noisy channels
- Reasoning on data words over numeric domains
- On runtime enforcement via suppressions
- Streaming Property Testing of Visibly Pushdown Languages *
- Sequentiality of string-to-context transducers
- Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines
- On the Model Checking Problem for Some Extension of CTL*
- Equivalence checking problem for finite state transducers over semigroups
- Extended symbolic finite automata and transducers
- Expressiveness of streaming string transducers
- Copyless cost-register automata: structure, expressiveness, and closure properties
- Regular Transformations of Data Words Through Origin Information
- Better complexity bounds for cost register automata
- Better complexity bounds for cost register automata
- An automata-theoretic approach to the verification of distributed algorithms
- Semantic Foundations for Deterministic Dataflow and Stream Processing
- Regular Programming for Quantitative Properties of Data Streams
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)
