Formal methods based on symbolic representations have been found to be very effective. In the case of infinite state systems, there has been a great deal of interest in accelerations - a technique for characterizing the result of iterating an execution sequence an arbitrary number of times, in a sound, but not necessarily complete, way. We propose the use of abstractions as a general framework to design accelerations. We investigate SemiLinear Regular Expressions (SLREs) as symbolic representations for FIFO automata. In particular, we show that SLREs are easy to manipulate (inclusion between two SLREs is in NP ∩ coNP), they form the core of known FIFO symbolic representations (SLREs = QDDs ∩ CQDDs), and they are usually sufficient since for FIFO automata with one channel, an arbitrary iteration of a loop is LRE representable. © Springer-Verlag Berlin Heidelberg 2000.
CITATION STYLE
Finkel, A., Iyer, P., & Sutre, G. (2000). Well-abstracted transition systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1877 LNCS, pp. 566–581). Springer Verlag. https://doi.org/10.1007/3-540-44618-4_40
Mendeley helps you to discover research relevant for your work.