@inproceedings{minisy2020mm,
    author     = {Mondok, Mil\'an and V\"or\"os, Andr\'as},
    title      = {Abstraction-Based Model Checking of Linear Temporal Properties},
    year       = {2020},
    booktitle  = {Proceedings of the 27th PhD Mini-Symposium},
    location   = {Budapest, Hungary},
    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},
    editor     = {Renczes, Bal\'azs},
    pages      = {29--32},

    type       = {Local event},
    url_pdf    = {minisy2020mm.pdf},
    abstract   = {Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of "lasso"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.},
}

{"_id":"ocxaehrHneLmE6Ect","bibbaseid":"mondok-vrs-abstractionbasedmodelcheckingoflineartemporalproperties-2020","authorIDs":[],"author_short":["Mondok, M.","Vörös, A."],"bibdata":{"bibtype":"inproceedings","type":"Local event","author":[{"propositions":[],"lastnames":["Mondok"],"firstnames":["Milán"],"suffixes":[]},{"propositions":[],"lastnames":["Vörös"],"firstnames":["András"],"suffixes":[]}],"title":"Abstraction-Based Model Checking of Linear Temporal Properties","year":"2020","booktitle":"Proceedings of the 27th PhD Mini-Symposium","location":"Budapest, Hungary","publisher":"Budapest University of Technology and Economics, Department of Measurement and Information Systems","editor":[{"propositions":[],"lastnames":["Renczes"],"firstnames":["Balázs"],"suffixes":[]}],"pages":"29–32","url_pdf":"minisy2020mm.pdf","abstract":"Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of \"lasso\"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.","bibtex":"@inproceedings{minisy2020mm,\n author = {Mondok, Mil\\'an and V\\\"or\\\"os, Andr\\'as},\n title = {Abstraction-Based Model Checking of Linear Temporal Properties},\n year = {2020},\n booktitle = {Proceedings of the 27th PhD Mini-Symposium},\n location = {Budapest, Hungary},\n publisher = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n editor = {Renczes, Bal\\'azs},\n pages = {29--32},\n\n type = {Local event},\n url_pdf = {minisy2020mm.pdf},\n abstract = {Even though the expressiveness of linear temporal logic (LTL) supports engineering application, model checking of such properties is a computationally complex task and state space explosion often hinders successful verification. LTL model checking consists of constructing automata from the property and the system, generating the synchronous product of the two automata and checking its language emptiness. We propose a novel LTL model checking algorithm that uses abstraction to tackle the challenge of state space explosion. This algorithm combines the advantages of two commonly used model checking approaches, counterexample-guided abstraction refinement and automata theoretic LTL model checking. The main challenge in combining these is the refinement of \"lasso\"-shaped counterexamples, for which task we propose a novel refinement strategy based on interpolation.},\n}\n\n","author_short":["Mondok, M.","Vörös, A."],"editor_short":["Renczes, B."],"key":"minisy2020mm","id":"minisy2020mm","bibbaseid":"mondok-vrs-abstractionbasedmodelcheckingoflineartemporalproperties-2020","role":"author","urls":{" pdf":"https://ftsrg.mit.bme.hu/theta/publications/minisy2020mm.pdf"},"metadata":{"authorlinks":{}},"downloads":17},"bibtype":"inproceedings","biburl":"https://ftsrg.mit.bme.hu/theta/publications/publications.bib","creationDate":"2020-02-17T09:08:37.075Z","downloads":17,"keywords":[],"search_terms":["abstraction","based","model","checking","linear","temporal","properties","mondok","vörös"],"title":"Abstraction-Based Model Checking of Linear Temporal Properties","year":2020,"dataSources":["7MDizr2BZojXoNdPN","eNuyx4kkedTyxecqY","ceR4xqaQusy7vTLW9"]}