DC Field | Value | Language |
---|---|---|
dc.contributor.author | Arias, Jaime | - |
dc.contributor.author | Olarte, Carlos | - |
dc.contributor.author | Petrucci, Laure | - |
dc.contributor.author | Bae, Kyungmin | - |
dc.contributor.author | Olveczky, Peter Csaba | - |
dc.date.accessioned | 2024-12-12T00:40:23Z | - |
dc.date.available | 2024-12-12T00:40:23Z | - |
dc.date.created | 2024-10-30 | - |
dc.date.issued | 2024-09 | - |
dc.identifier.issn | 0169-2968 | - |
dc.identifier.uri | https://oasis.postech.ac.kr/handle/2014.oak/125035 | - |
dc.description.abstract | This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude- including full LTL model checking, analysis with user-defined execution strategies, and even statistical model checking-for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Rom & eacute;o can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Rom & eacute;o in many cases. | - |
dc.language | English | - |
dc.publisher | IOS Press | - |
dc.relation.isPartOf | Fundamenta Informaticae | - |
dc.title | A Rewriting-logic-with-SMT-based Formal Analysis and Parameter Synthesis Framework for Parametric Time Petri Nets | - |
dc.type | Article | - |
dc.identifier.doi | 10.3233/FI-242195 | - |
dc.type.rims | ART | - |
dc.identifier.bibliographicCitation | Fundamenta Informaticae, v.192, no.3-4, pp.261 - 312 | - |
dc.identifier.wosid | 001325906300003 | - |
dc.citation.endPage | 312 | - |
dc.citation.number | 3-4 | - |
dc.citation.startPage | 261 | - |
dc.citation.title | Fundamenta Informaticae | - |
dc.citation.volume | 192 | - |
dc.contributor.affiliatedAuthor | Bae, Kyungmin | - |
dc.description.journalClass | 1 | - |
dc.description.journalClass | 1 | - |
dc.description.isOpenAccess | N | - |
dc.type.docType | Article | - |
dc.subject.keywordPlus | REAL-TIME | - |
dc.subject.keywordPlus | MODEL-CHECKING | - |
dc.subject.keywordPlus | SPECIFICATION | - |
dc.subject.keywordPlus | SEMANTICS | - |
dc.subject.keywordPlus | SYSTEMS | - |
dc.subject.keywordAuthor | parametric timed Petri nets | - |
dc.subject.keywordAuthor | rewriting logic | - |
dc.subject.keywordAuthor | Maude | - |
dc.subject.keywordAuthor | SMT | - |
dc.subject.keywordAuthor | parameter synthesis | - |
dc.subject.keywordAuthor | symbolic reachability analysis | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Software Engineering | - |
dc.relation.journalWebOfScienceCategory | Mathematics, Applied | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
library@postech.ac.kr Tel: 054-279-2548
Copyrights © by 2017 Pohang University of Science ad Technology All right reserved.