liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Ordered Counter-Abstraction Refinable Subword Relations for Parameterized Verification
IMDEA Software Institute, Spain.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
2014 (English)In: LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2014), Springer Berlin/Heidelberg, 2014, Vol. 8370, 396-408 p.Conference paper (Refereed)
Abstract [en]

We present an original refinable subword based symbolic representation for the verification of linearly ordered parameterized systems. Such a system consists of arbitrary many finite processes placed in an array. Processes communicate using global transitions constrained by their relative positions (i.e., priorities). The model can include binary communication, broadcast, shared variables or dynamic creation and deletion of processes. Configurations are finite words of arbitrary lengths. The successful monotonic abstraction approach uses the subword relation to define upward closed sets as symbolic representations for such systems. Natural and automatic refinements remained missing for such symbolic representations. For instance, subword based relations are simply too coarse for automatic forward verification of systems involving priorities. We remedy to this situation and introduce a symbolic representation based on an original combination of counter abstraction with subword based relations. This allows us to define an infinite family of relaxation operators that guarantee termination by a new well quasi ordering argument. The proposed automatic analysis is at least as precise and efficient as monotonic abstraction when performed backwards. It can also be successfully used in forward, something monotonic abstraction is incapable of. We implemented a prototype to illustrate the approach.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2014. Vol. 8370, 396-408 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online) ; 8370
Keyword [en]
counter abstraction; well quasi ordering; reachability; parameterized verification
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:liu:diva-117675DOI: 10.1007/978-3-319-04921-2_32ISI: 000352688800032ScopusID: 2-s2.0-84898069230ISBN: 978-3-319-04921-2ISBN: 978-3-319-04920-5OAI: oai:DiVA.org:liu-117675DiVA: diva2:811277
Conference
8th International Conference on Language and Automata Theory and Applications (LATA)
Available from: 2015-05-11 Created: 2015-05-06 Last updated: 2016-08-22

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Rezine, Ahmed
By organisation
Software and SystemsThe Institute of Technology
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 40 hits
ReferencesLink to record
Permanent link

Direct link