mycoreobjectrosdok_disshab_0000002613rosdok_disshab_0000002613rosdokdisshabrosdok_derivate_00001058622023-08-08T10:13:26.080Z2021-10-19T09:25:53.064ZadministratoreditorMSpublished1rosdok_derivate_0000105862truetruederivate_types:fulltextVolltextfulltextwf_edit_epub wf_register_epubstate:publishedstate:publishedveröffentlichtpublishedrosdok/id000032711774469006Oau2021-10-192023-08-05T19:18:27ZrdaConverted from PICA to MODS using Pica2Mods XSLT Transformer 2.7 [SCM: "0c0e7a3c226a4a0cbcbec39b493c3c5257339ab8" "v2.7" "2023-08-04T00:00:00+0200"] with mode 'DEFAULT'.DissertationHochschulschriftImproving explicit model checking for Petri netsModel checking is the automated verification that systematically checks if a given behavioral property holds for a given model of a system. We use Petri nets and temporal logic as formalisms to describe a system and its behavior in a mathematically precise and unambiguous manner. The contributions of this thesis are concerned with the improvement of model checking efficiency both in theory and in practice. We present two new reduction techniques and several supplementary strength reduction techniques. The thesis also enhances partial order reduction for certain temporal logic classes.TorstenLiebke1985 -VerfasserInaut1243527919KarstenWolf1967 -AkademischeR BetreuerIndgs124773052University of Rostock, GermanyJiriSrbaAkademischeR BetreuerIndgsUniversity of Aalborg, Denmark38329-6Universität Rostock1419 -Grad-verleihende Institutiondgg10085032-7Universität RostockFakultät für Informatik und Elektrotechnik2004 -Grad-verleihende Institutiondgghttp://purl.uni-rostock.de/rosdok/id00003271urn:nbn:de:gbv:28-rosdok_id00003271-310.18453/rosdok_id00003271004 InformatikFakultät für Informatik und ElektrotechnikCC BY 4.0Nutzungsrechte erteiltLizenz Metadaten: CC0frei zugänglich (Open Access)en2020Universität RostockRostockmonographic202120202021Universitätsbibliothek RostockRostock2021Universitätsbibliothek Rostockhttp://purl.uni-rostock.de/rosdok/id00003271Karsten Wolf (University of Rostock, Germany) ; Jiri Srba (University of Aalborg, Denmark)[{"affil":"University of Rostock, Germany","name":"Wolf, Karsten"},{"affil":"University of Aalborg, Denmark","name":"Srba, Jiri"}]vorgelegt von Torsten LiebkeUniversity of Rostock, GermanyWolf, KarstenUniversity of Aalborg, DenmarkSrba, Jiridoctype:epubdoctype:epubDokumenttypDocument typedoctype:epub.dissertationdoctype:epub.dissertationDissertationdoctoral thesisdiniPublType:doctoralThesis diniPublType2022:PhDThesis XMetaDissPlusThesisLevel:thesis.doctoralinfo:eu-repo/semantics/doctoralThesisdocumentnatureOfContent:ppn_105825778natureOfContent:ppn_105825778HochschulschriftdiniPublType2022:DoctoralThesisdiniPublType2022:DoctoralThesisDissertation oder HabilitationDoctoral thesisDRIVERdiniPublType2022:PhDThesisdiniPublType2022:PhDThesisDissertationPhD thesisKDSF (Pu34)XMetaDissPlusThesisLevel:thesis.doctoralXMetaDissPlusThesisLevel:thesis.doctoralDoktorarbeitdoctoral thesisSDNB:004SDNB:004004 Informatik004 Data processing Computer sciencesinstitution:unirostockinstitution:unirostockUniversität RostockUniversity of RostockUniversität RostockUniversität RostockUni.Rostockhttp://d-nb.info/gnd/38329-6institution:unirostock.iefinstitution:unirostock.iefFakultät für Informatik und ElektrotechnikFaculty of Computer Science and Electrical EngineeringUniversität Rostock. Fakultät für Informatik und ElektrotechnikFakultät für Informatik<br />und ElektrotechnikUni.Rostock.Fakultaet.IEFhttp://d-nb.info/gnd/10085032-7licenseinfo:worklicenseinfo:workWerkworklicenseinfo:work.cclicenselicenseinfo:work.cclicenseCC-LizenzCC-licenselicenseinfo:work.cclicense.cc-bylicenseinfo:work.cclicense.cc-byCC BYCC BYlicenseinfo:work.cclicense.cc-by.v40licenseinfo:work.cclicense.cc-by.v40CC BY 4.0CC BY 4.0/creativecommons/l/by/4.0/88x31.png[DE-28]Namensnennung 4.0 International$cCC BY 4.0$gCreative Commons$uhttps://creativecommons.org/licenses/by/4.0/https://creativecommons.org/licenses/by/4.0/https://creativecommons.org/licenses/by/4.0/licenseinfo:depositlicenseinfo:depositVeröffentlichungsgenehmigungpermission to storelicenseinfo:deposit.rightsgrantedlicenseinfo:deposit.rightsgrantedNutzungsrechte erteiltrights grantedlicenseinfo:metadatalicenseinfo:metadataLizenzen für Metadatenlicenseinfo:metadata.cc0licenseinfo:metadata.cc0Lizenz Metadaten: CC0license metadata: CC0/creativecommons/p/zero/1.0/88x31.pnghttps://creativecommons.org/publicdomain/zero/1.0/accesscondition:openaccessaccesscondition:openaccessfrei zugänglich (Open Access)open accesshttp://purl.org/coar/access_right/c_abf2OAfreeinfo:eu-repo/semantics/openAccess[DE-28]Open Access$gControlled Vocabulary for Access Rights$uhttp://purl.org/coar/access_right/c_abf2rfc5646:enrfc5646:enEnglischEnglishengengImproving explicit model checking for Petri netsImproving explicit model checking for Petri netsgnd:1243527919gnd:124773052gnd:38329-6gnd:10085032-7gnd:1243527919gnd:124773052gnd:38329-6gnd:10085032-7rosdok_disshab_0000002613-d777599e52gnd:1243527919Torsten LiebkeTorsten Liebkerosdok_disshab_0000002613-d777599e66gnd:124773052Karsten WolfKarsten Wolfrosdok_disshab_0000002613-d777599e81Jiri SrbaJiri Srbarosdok_disshab_0000002613-d777599e92gnd:38329-6Universität RostockUniversität Rostockrosdok_disshab_0000002613-d777599e104gnd:10085032-7Universität Rostock Fakultät für Informatik und ElektrotechnikUniversität Rostock Fakultät für Informatik und ElektrotechnikTorsten LiebkeKarsten WolfJiri SrbaUniversität RostockUniversität Rostock Fakultät für Informatik und ElektrotechnikTorsten LiebkeKarsten WolfJiri SrbaUniversität RostockUniversität Rostock Fakultät für Informatik und ElektrotechnikTorsten LiebkeRostockUniversität Rostockepub.dissertationhttp://purl.uni-rostock.de/rosdok/id00003271urn:nbn:de:gbv:28-rosdok_id00003271-310.18453/rosdok_id00003271Model checking is the automated verification that systematically checks if a given behavioral property holds for a given model of a system. We use Petri nets and temporal logic as formalisms to describe a system and its behavior in a mathematically precise and unambiguous manner. The contributions of this thesis are concerned with the improvement of model checking efficiency both in theory and in practice. We present two new reduction techniques and several supplementary strength reduction techniques. The thesis also enhances partial order reduction for certain temporal logic classes.20202020Karsten Wolf (University of Rostock, Germany) ; Jiri Srba (University of Aalborg, Denmark)[{"affil":"University of Rostock, Germany","name":"Wolf, Karsten"},{"affil":"University of Aalborg, Denmark","name":"Srba, Jiri"}]vorgelegt von Torsten Liebkeepub.dissertation1 Liebke_Dissertation_2021.pdf 1725444 eceb0e361c4e655b77002f2961c8c93f rosdok/id000032711774469006Oau2021-10-192023-08-05T19:18:27ZrdaConverted from PICA to MODS using Pica2Mods XSLT Transformer 2.7 [SCM: "0c0e7a3c226a4a0cbcbec39b493c3c5257339ab8" "v2.7" "2023-08-04T00:00:00+0200"] with mode 'DEFAULT'.DissertationHochschulschriftImproving explicit model checking for Petri netsModel checking is the automated verification that systematically checks if a given behavioral property holds for a given model of a system. We use Petri nets and temporal logic as formalisms to describe a system and its behavior in a mathematically precise and unambiguous manner. The contributions of this thesis are concerned with the improvement of model checking efficiency both in theory and in practice. We present two new reduction techniques and several supplementary strength reduction techniques. The thesis also enhances partial order reduction for certain temporal logic classes.TorstenLiebke1985 -VerfasserInaut1243527919KarstenWolf1967 -AkademischeR BetreuerIndgs124773052University of Rostock, GermanyJiriSrbaAkademischeR BetreuerIndgsUniversity of Aalborg, Denmark38329-6Universität Rostock1419 -Grad-verleihende Institutiondgg10085032-7Universität RostockFakultät für Informatik und Elektrotechnik2004 -Grad-verleihende Institutiondgghttp://purl.uni-rostock.de/rosdok/id00003271urn:nbn:de:gbv:28-rosdok_id00003271-310.18453/rosdok_id00003271004 InformatikFakultät für Informatik und ElektrotechnikCC BY 4.0Nutzungsrechte erteiltLizenz Metadaten: CC0frei zugänglich (Open Access)en2020Universität RostockRostockmonographic202120202021Universitätsbibliothek RostockRostock2021Universitätsbibliothek Rostockhttp://purl.uni-rostock.de/rosdok/id00003271Karsten Wolf (University of Rostock, Germany) ; Jiri Srba (University of Aalborg, Denmark)[{"affil":"University of Rostock, Germany","name":"Wolf, Karsten"},{"affil":"University of Aalborg, Denmark","name":"Srba, Jiri"}]vorgelegt von Torsten Liebke University of Rostock, Germany Wolf, Karsten University of Aalborg, Denmark Srba, Jiri 2021-10-19T09:25:53.064Z 2023-08-08T10:13:26.080Z 2023-08-18T10:13:26.085Z {"identifier":"rosdok/id00003271","type":"local_id","additional":"","service":"MCRLocalID","created":"2021-10-19T09:25:53.085Z","registered":"2021-10-19T09:25:53.085Z"} editorMS {"identifier":"urn:nbn:de:gbv:28-rosdok_id00003271-3","type":"dnbUrn","additional":"","service":"RosDokURN","created":"2021-10-19T09:25:53.097Z","registered":"2021-10-19T15:33:57.627Z"} administratorfulltextfile/rosdok_disshab_0000002613/rosdok_derivate_0000105862/Liebke_Dissertation_2021.pdfImproving explicit model checking for Petri netsImproving explicit model checking for Petri netsgnd:1243527919gnd:124773052gnd:38329-6gnd:10085032-7gnd:1243527919gnd:124773052gnd:38329-6gnd:10085032-7rosdok_disshab_0000002613-d777599e52gnd:1243527919Torsten LiebkeTorsten Liebkerosdok_disshab_0000002613-d777599e66gnd:124773052Karsten WolfKarsten Wolfrosdok_disshab_0000002613-d777599e81Jiri SrbaJiri Srbarosdok_disshab_0000002613-d777599e92gnd:38329-6Universität RostockUniversität Rostockrosdok_disshab_0000002613-d777599e104gnd:10085032-7Universität Rostock Fakultät für Informatik und ElektrotechnikUniversität Rostock Fakultät für Informatik und ElektrotechnikTorsten LiebkeKarsten WolfJiri SrbaUniversität RostockUniversität Rostock Fakultät für Informatik und ElektrotechnikTorsten LiebkeKarsten WolfJiri SrbaUniversität RostockUniversität Rostock Fakultät für Informatik und ElektrotechnikTorsten LiebkeRostockUniversität Rostockepub.dissertationhttp://purl.uni-rostock.de/rosdok/id00003271urn:nbn:de:gbv:28-rosdok_id00003271-310.18453/rosdok_id00003271Model checking is the automated verification that systematically checks if a given behavioral property holds for a given model of a system. We use Petri nets and temporal logic as formalisms to describe a system and its behavior in a mathematically precise and unambiguous manner. The contributions of this thesis are concerned with the improvement of model checking efficiency both in theory and in practice. We present two new reduction techniques and several supplementary strength reduction techniques. The thesis also enhances partial order reduction for certain temporal logic classes.20202020Karsten Wolf (University of Rostock, Germany) ; Jiri Srba (University of Aalborg, Denmark)[{"affil":"University of Rostock, Germany","name":"Wolf, Karsten"},{"affil":"University of Aalborg, Denmark","name":"Srba, Jiri"}]vorgelegt von Torsten Liebke[xslt]Saxonrosdok/id00003271https://purl.uni-rostock.de/rosdok/id00003271177446900610.18453/rosdok_id00003271urn:nbn:de:gbv:28-rosdok_id00003271-3Torsten LiebkeLiebke TorstenImproving explicit model checking for Petri netsDissertationdoctoral thesisUniversität Rostock, 2020Model checking is the automated verification that systematically checks if a given behavioral property holds for a given model of a system. We use Petri nets and temporal logic as formalisms to describe a system and its behavior in a mathematically precise and unambiguous manner. The contributions…Torsten LiebkeImproving explicit model checking for Petri netsUniversitätsbibliothek Rostockhttp://purl.uni-rostock.de/rosdok/id00003271TorstenLiebke1985 -VerfasserInaut1243527919KarstenWolf1967 -AkademischeR BetreuerIndgs124773052University of Rostock, GermanyJiriSrbaAkademischeR BetreuerIndgsUniversity of Aalborg, Denmark38329-6Universität Rostock1419 -Grad-verleihende Institutiondgg10085032-7Universität RostockFakultät für Informatik und Elektrotechnik2004 -Grad-verleihende Institutiondgg[purl]http://purl.uni-rostock.de/rosdok/id00003271[urn]urn:nbn:de:gbv:28-rosdok_id00003271-3[doi]10.18453/rosdok_id00003271open_access20202020epoch:21th_centuryrfc5646:endoctype:epub.dissertationaccesscondition:openaccessSDNB:004institution:unirostock.iefstate:published