dc.contributor.author | Neele, Thomas | |
dc.contributor.author | Willemse, Tim A. C. | |
dc.contributor.author | Wesselink, Wieger | |
dc.contributor.author | Valmari, Antti | |
dc.date.accessioned | 2022-10-06T10:18:00Z | |
dc.date.available | 2022-10-06T10:18:00Z | |
dc.date.issued | 2022 | |
dc.identifier.citation | Neele, T., Willemse, T. A. C., Wesselink, W., & Valmari, A. (2022). Partial-order reduction for parity games and parameterised Boolean equation systems. <i>International Journal on Software Tools for Technology Transfer</i>, <i>24</i>(5), 735-756. <a href="https://doi.org/10.1007/s10009-022-00672-0" target="_blank">https://doi.org/10.1007/s10009-022-00672-0</a> | |
dc.identifier.other | CONVID_156894312 | |
dc.identifier.uri | https://jyx.jyu.fi/handle/123456789/83478 | |
dc.description.abstract | In model checking, reduction techniques can be helpful tools to fight the state-space explosion problem. Partial-order reduction (POR) is a well-known example, and many POR variants have been developed over the years. However, none of these can be used in the context of model checking stutter-sensitive temporal properties. We propose POR techniques for parity games, a well-established formalism for solving a variety of decision problems, including model checking. As a result, we obtain the first POR method that is sound for the full modal μ-calculus. We show how our technique can be applied to the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments with our implementation indicate that substantial reductions can be achieved. | en |
dc.format.mimetype | application/pdf | |
dc.language.iso | eng | |
dc.publisher | Springer | |
dc.relation.ispartofseries | International Journal on Software Tools for Technology Transfer | |
dc.rights | CC BY 4.0 | |
dc.subject.other | partial-order reduction | |
dc.subject.other | parity games | |
dc.subject.other | parameterised Boolean equation systems | |
dc.subject.other | stubborn sets | |
dc.title | Partial-order reduction for parity games and parameterised Boolean equation systems | |
dc.type | research article | |
dc.identifier.urn | URN:NBN:fi:jyu-202210064808 | |
dc.contributor.laitos | Informaatioteknologian tiedekunta | fi |
dc.contributor.laitos | Faculty of Information Technology | en |
dc.contributor.oppiaine | Tietojenkäsittelytiede | fi |
dc.contributor.oppiaine | Tutkintokoulutus | fi |
dc.contributor.oppiaine | Computer Science | en |
dc.contributor.oppiaine | Degree Education | en |
dc.type.uri | http://purl.org/eprint/type/JournalArticle | |
dc.type.coar | http://purl.org/coar/resource_type/c_2df8fbb1 | |
dc.description.reviewstatus | peerReviewed | |
dc.format.pagerange | 735-756 | |
dc.relation.issn | 1433-2779 | |
dc.relation.numberinseries | 5 | |
dc.relation.volume | 24 | |
dc.type.version | publishedVersion | |
dc.rights.copyright | © The Author(s) 2022 | |
dc.rights.accesslevel | openAccess | fi |
dc.type.publication | article | |
dc.subject.yso | tietojenkäsittely | |
dc.subject.yso | peliteoria | |
dc.subject.yso | Boolen algebra | |
dc.subject.yso | verifiointi | |
dc.format.content | fulltext | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p2407 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p13476 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p762 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p6609 | |
dc.rights.url | https://creativecommons.org/licenses/by/4.0/ | |
dc.relation.doi | 10.1007/s10009-022-00672-0 | |
dc.type.okm | A1 | |