{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,26]],"date-time":"2026-06-26T09:40:55Z","timestamp":1782466855011,"version":"3.54.5"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2007,3,1]],"date-time":"2007-03-01T00:00:00Z","timestamp":1172707200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2007,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We develop a model of parametric probabilistic transition Systems (PPTSs), where probabilities associated with transitions may be parameters. We show how to find instances of the parameters that satisfy a given property and instances that either maximize or minimize the probability of reaching a certain state. As an application, we model a probabilistic non-repudiation protocol with a PPTS. The theory we develop allows us to find instances that maximize the probability that the protocol ends in a fair state (no participant has an advantage over the others).<\/jats:p>","DOI":"10.1007\/s00165-006-0015-2","type":"journal-article","created":{"date-parts":[[2006,11,29]],"date-time":"2006-11-29T18:23:33Z","timestamp":1164824613000},"page":"93-109","source":"Crossref","is-referenced-by-count":57,"title":["Parametric probabilistic transition systems for system design and analysis"],"prefix":"10.1145","volume":"19","author":[{"given":"Ruggero","family":"Lanotte","sequence":"first","affiliation":[{"name":"Dipartimento di Scienze della Cultura, Politiche e dell\u2019Informazione, Universit\u00e0 dell\u2019Insubria, Via Valleggio 11, 22100, Como, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrea","family":"Maggiolo-Schettini","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e1 di pisa, Largo Pontecorvo 3, 56127, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Angelo","family":"Troina","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e1 di pisa, Largo Pontecorvo 3, 56127, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Aldini A Gorrieri R (2002) Security analysis of a probabilistic non-repudiation protocol. In: Proceedings. of PAPM-PROBMIV\u201902 Springer LNCS 2399 pp 17\u201336","DOI":"10.1007\/3-540-45605-8_3"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"de Alfaro L (1998) How to specify and verify the long-run average behaviour of probabilistic systems. In: Proceedings of LICS\u201998 IEEE pp 454\u2013465","DOI":"10.1109\/LICS.1998.705679"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"de Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Proceedings. of CONCUR\u201999 Springer LNCS 1664 pp 66\u201381","DOI":"10.1007\/3-540-48320-9_7"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Alur R Henzinger TA Vardi MY (1993) Parametric real-time reasoning. In: Proceedings. of STOC\u201993 ACM pp 592\u2013601","DOI":"10.1145\/167088.167242"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Amnell T Behrmann G Bengtsson J D\u2019Argenio PR David A Fehnker A Hune T Jeannet B Larsen KG Moeller MO Pettersson P Weise C Yi W (2000) Uppaal-now next and future. In: Proceedings. of MOVEP\u201900 Springer LNCS 2067 pp 99\u2013124","DOI":"10.1007\/3-540-45510-8_4"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1135"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00038-6"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050046"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FUN-2002-50101","article-title":"Markov decision processes and Buchi automata","volume":"50","author":"Beauquier D","year":"2002","journal-title":"Fundam Inform"},{"key":"e_1_2_1_2_11_2","volume-title":"Dynamic programming","author":"Bellman RE","year":"1957"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bianco A de Alfaro L (1995) Model checking of probabilistic and deterministic systems. In: Proceedings of 15th Conference on foundations of computer technology and theoretical computer science Springer LNCS 1026 pp 499\u2013513","DOI":"10.1007\/3-540-60692-0_70"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Bohnenkamp H van der Stok P Hermanns H Vaandrager F (2003) Costoptimization of the IPv4 zeroconf protocol. In: Proceedings of DSN\u201903 IEEE pp 531\u2013540","DOI":"10.1109\/DSN.2003.1209963"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00206326"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Cleaveland R Smolka SA Zwarico A (1992) Testing preorders for probabilistic processes. In: Proceedings of ICALP\u201992 Springer LNCS 623 pp 708\u2013719","DOI":"10.1007\/3-540-55719-9_116"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Daws C (2004) Symbolic and parametric model checking of discrete-time markov Chains. In: Proceedings of ICTAC\u201904 Springer LNCS 3407 pp 280\u2013294","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Deng Y Chothia T Palamidessi C Pang J (2006) Metrics for Action-labelled Quantitative Transition Systems. In: Proceedings of QAPL\u201905 Elsevier ENTCS 153(2) pp 79\u201396","DOI":"10.1016\/j.entcs.2005.10.033"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Desharnais J Jagadeesan R Gupta V Panangaden P (2002) The metric analogue of weak bisimulation for probabilistic processes . In: Proceedings of LICS\u201902 IEEE pp 413\u2013422","DOI":"10.1109\/LICS.2002.1029849"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"e_1_2_1_2_20_2","unstructured":"Desharnais J Edalat A Panangaden P (1998) A logic characterization of bisimulation for Markov Processes. In: Proceedings of LICS\u201998 IEEE 478\u2013487"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00051-8"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9440-2"},{"key":"e_1_2_1_2_23_2","volume-title":"Time and probability in formal design of distributed systems. Real-time safety critical systems 1","author":"Hansson H","year":"1994"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Henzinger TA Ho P-H Wong-Toi H (1997) HyTech: a model checker for hybrid systems. In: Proceedings of CAV\u201997 Springer LNCS 1254 pp 460\u2013463","DOI":"10.1007\/3-540-63166-6_48"},{"key":"e_1_2_1_2_26_2","volume-title":"Dynamic programming and Markov processes","author":"Howard H","year":"1960"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hune T Romijn J Stoelinga M Vaandrager FW (1960) Linear parametric model checking of timed automata. J Log Algebr Program 52\u201353: 183\u2013220","DOI":"10.1016\/S1567-8326(02)00037-1"},{"key":"e_1_2_1_2_28_2","unstructured":"Jonsson B Larsen K (1991) Specification and refinement of probabilistic processes. In: Proceedings of LICS\u201991 IEEE pp 266\u2013277"},{"key":"e_1_2_1_2_29_2","unstructured":"Kemeny J Snell J Knapp A (1996) Denumerable Markov chains. D. Van Nostrand Company Inc."},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Lanotte R Maggiolo-Schettini A Troina A (2003) Weak bisimulation for probabilistic timed automata and applications to security. In: Proceedings of SEFM\u201903 IEEE pp 34\u201343","DOI":"10.1109\/SEFM.2003.1236205"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Lanotte R Maggiolo-Schettini A Troina A (2004) Decidability results for parametric probabilistic transition systems with an application to security. In: Proceedings of SEFM\u201904 IEEE pp 114\u2013121","DOI":"10.1109\/SEFM.2004.1347512"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Lanotte R Maggiolo-Schettini A Troina A (2005) Automatic analysis of a non-repudiation protocol. In: Proceedings of QAPL\u201903 Elsevier ENTCS 112 pp 113\u2013129","DOI":"10.1016\/j.entcs.2004.01.020"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00004-G"},{"key":"e_1_2_1_2_35_2","unstructured":"Markowitch O Roggeman Y (1999) Probabilistic non-repudiation without trusted third party. In: Proceedings of 2nd Conference on Security in Communication Network"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/49.668972"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/290163.290168"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(10)80003-3"},{"key":"e_1_2_1_2_39_2","volume-title":"Stochastic processes","author":"Ross S","year":"1983"},{"key":"e_1_2_1_2_40_2","unstructured":"Stark E Smolka SA (1998) Compositional analysis of expected delays in networks of probabilistic I\/O automata. In: Proceedings of LICS 98 IEEE pp 466\u2013477"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-009-0839-0","volume-title":"Galois theory","author":"Stewart I","year":"1989"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","first-page":"3007","DOI":"10.1093\/ietfec\/e88-a.11.3007","article-title":"double depth first search based parametric analysis for parametric time\u2013interval automata","volume":"11","author":"Tanimoto T","year":"2005","journal-title":"IEICE Trans Fundam"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Tarski A (1951) A Decision method for elementary algebra and geometry 2nd edn. University of California Press","DOI":"10.1525\/9780520348097"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813658"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00056-X"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-006-0015-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-006-0015-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-006-0015-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T05:33:37Z","timestamp":1736660017000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-006-0015-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,3]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,3]]}},"alternative-id":["10.1007\/s00165-006-0015-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-006-0015-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,3]]}}}