Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-319-06410-9-29
Title: Compositional synthesis of concurrent systems through causal model checking and learning
Authors: Lin, S.-W. 
Hsiung, P.-A.
Issue Date: 2014
Citation: Lin, S.-W.,Hsiung, P.-A. (2014). Compositional synthesis of concurrent systems through causal model checking and learning. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8442 LNCS : 416-431. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-319-06410-9-29
Abstract: Formal verification such as model checking can be used to verify whether a system model satisfies a given specification. However, if model checking shows that the system model violates the specification, the designer has to manually refine the system model. To automate this refinement process, we propose a learning-based synthesis framework that can automatically eliminate all counterexamples from a system model based on causality semantics such that the synthesized model satisfies a given safety specification. Further, the framework for synthesis is not only automatic, but is also an iterative compositional process based on the L algorithm, i.e., the global state space of the system is never generated in the synthesis process. We also prove the correctness and termination of the synthesis framework. © 2014 Springer International Publishing Switzerland.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/117236
ISBN: 9783319064093
ISSN: 16113349
DOI: 10.1007/978-3-319-06410-9-29
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

89
checked on Jan 16, 2021

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.