{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article10154","name":"Coverability Synthesis in Parametric Petri Nets","abstract":"We study Parametric Petri Nets (PPNs), i.e., Petri nets for which some arc weights can be parameters. In that setting, we address a problem of parameter synthesis, which consists in computing the exact set of values for the parameters such that a given marking is coverable in the instantiated net.\r\n\r\nSince the emptiness of that solution set is already undecidable for general PPNs, we address a special case where parameters are used only as input weights (preT-PPNs), and consequently for which the solution set is\r\ndownward-closed. To this end, we invoke a result for the representation of \r\nupward closed set from Valk and Jantzen. \r\nTo use this procedure, we show we need to decide universal coverability, \r\nthat is decide if some marking is coverable for every possible values of the parameters.\r\nWe therefore provide a proof of its EXPSPACE-completeness,\r\nthus settling the previously open problem of its decidability.\r\n \r\nWe also propose an adaptation of this reasoning to the case of\r\nparameters used only as output weights (postT-PPNs).\r\nIn this case, the condition to use this procedure can be reduced to the decidability of the existential coverability, \r\nthat is decide if there exists values of the parameters making a given marking coverable. \r\nThis problem is known decidable but we provide here a cleaner proof, providing its EXPSPACE-completeness, by reduction to Omega Petri Nets.","keywords":["Petri net","Parameters","Coverability","Unboundedness","Synthesis"],"author":[{"@type":"Person","name":"David, Nicolas","givenName":"Nicolas","familyName":"David"},{"@type":"Person","name":"Jard, Claude","givenName":"Claude","familyName":"Jard"},{"@type":"Person","name":"Lime, Didier","givenName":"Didier","familyName":"Lime"},{"@type":"Person","name":"Roux, Olivier H.","givenName":"Olivier H.","familyName":"Roux"}],"position":14,"pageStart":"14:1","pageEnd":"14:16","dateCreated":"2017-09-01","datePublished":"2017-09-01","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"David, Nicolas","givenName":"Nicolas","familyName":"David"},{"@type":"Person","name":"Jard, Claude","givenName":"Claude","familyName":"Jard"},{"@type":"Person","name":"Lime, Didier","givenName":"Didier","familyName":"Lime"},{"@type":"Person","name":"Roux, Olivier H.","givenName":"Olivier H.","familyName":"Roux"}],"copyrightYear":"2017","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.14","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume6288","volumeNumber":85,"name":"28th International Conference on Concurrency Theory (CONCUR 2017)","dateCreated":"2017-09-01","datePublished":"2017-09-01","editor":[{"@type":"Person","name":"Meyer, Roland","givenName":"Roland","familyName":"Meyer"},{"@type":"Person","name":"Nestmann, Uwe","givenName":"Uwe","familyName":"Nestmann"}],"isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article10154","isPartOf":{"@type":"Periodical","@id":"#series116","name":"Leibniz International Proceedings in Informatics","issn":"1868-8969","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume6288"}}}