From Natural Projection to Partial Model Checking and Back
OPEN ACCESS
Author / Producer
Date
2018
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Specification decomposition is a theoretically interesting and practically relevant problem for which two approaches were independently developed by the control theory and verification communities: natural projection and partial model checking. In this paper we show that, under reasonable assumptions, natural projection reduces to partial model checking and, when cast in a common setting, the two are equivalent. Aside from their theoretical interest, our results build a bridge whereby the control theory community can reuse algorithms and results developed by the verification community. In addition, we present an algorithm and a tool for the partial model checking of finite-state automata that can be used as an alternative to natural projection.
Permanent link
Publication status
published
External links
Book title
Tools and Algorithms for the Construction and Analysis of Systems. 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I
Journal / series
Volume
10805
Pages / Article No.
344 - 361
Publisher
Springer
Event
24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03634 - Basin, David / Basin, David