Please use this identifier to cite or link to this item:
|Title:||Compositional synthesis of concurrent systems through causal model checking and learning||Authors:||Lin, S.-W.
|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.
checked on Jan 16, 2021
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.