Parameterized Verification under TSO with Data Types
Formal Languages and Automata Theory
2023-02-14 v3 Programming Languages
Abstract
We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type. We use the translation to obtain tight complexity bounds for TSO-based parameterized verification over several abstract data types, such as push-down automata, ordered multi push-down automata, one-counter nets, one-counter automata, and Petri nets. We apply the framework to get complexity bounds for higher order stack and counter variants as well.
Cite
@article{arxiv.2302.02163,
title = {Parameterized Verification under TSO with Data Types},
author = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Florian Furbach and Adwait Godbole and Yacoub G. Hendi and Shankaranarayanan Krishna and Stephan Spengler},
journal= {arXiv preprint arXiv:2302.02163},
year = {2023}
}