{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:40:03Z","timestamp":1694623203086},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2004,11,1]],"date-time":"2004-11-01T00:00:00Z","timestamp":1099267200000},"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":[[2004,11]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            Formal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification\n            <jats:bold>A<\/jats:bold>\n            to a concrete specification\n            <jats:bold>C<\/jats:bold>\n            that is as least as deterministic. Knowing\n            <jats:bold>A<\/jats:bold>\n            and\n            <jats:bold>C<\/jats:bold>\n            one proves that\n            <jats:bold>C<\/jats:bold>\n            refines, or implements, specification\n            <jats:bold>A<\/jats:bold>\n            . In this study we consider specification\n            <jats:bold>A<\/jats:bold>\n            as given and concern ourselves with a way to find a good candidate for implementation\n            <jats:bold>C<\/jats:bold>\n            . To this end we classify all implementations of an abstract specification according to their performance. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification correctly are excluded. Only the remaining correct implementations\n            <jats:bold>C<\/jats:bold>\n            are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary for the performance of any implementation. We introduce the probabilistic action system formalism which combines refinement with performance. In our current study we measure performance in terms of long-run expected average-cost. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. A corresponding notion of refinement and simulation-based proof rules are introduced. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification\n            <jats:bold>A<\/jats:bold>\n            thus assisting in the search for a good implementation\n            <jats:bold>C<\/jats:bold>\n            .\n          <\/jats:p>","DOI":"10.1007\/s00165-004-0037-6","type":"journal-article","created":{"date-parts":[[2004,4,27]],"date-time":"2004-04-27T06:58:17Z","timestamp":1083049097000},"page":"313-331","source":"Crossref","is-referenced-by-count":4,"title":["Performance analysis of probabilistic action systems"],"prefix":"10.1145","volume":"16","author":[{"given":"Stefan","family":"Hallerstede","sequence":"first","affiliation":[{"name":"University of Southampton, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[{"name":"University of Southampton, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"The B-Book: assigning programs to meanings","author":"Abr J-R","year":"1996"},{"key":"p_2","first-page":"83","volume-title":"Bert D (ed) B'98: the 2nd international B conference, vol 1393 of lecture notes in computer science, LIRRM Laboratoire d'Informatique, de Robotique et de Micro-\u00e9lectronique de Montpellier","author":"Abrial J-R","year":"1998"},{"key":"p_3","first-page":"23","volume-title":"Vissers CA, Diaz M (eds) The formal description technique LOTOS","author":"Bolognesi T","year":"1989"},{"key":"p_4","doi-asserted-by":"crossref","unstructured":"[BCSS98] Bernardo M Cleaveland WR Sims ST Stewart WJ (1998) TwoTowers: a tool integrating functional and performance analysis of concurrent systems. In: Budkowski S Cavalli A Najm E (eds) Proceedings of the IFIP joint international conference on formal description techniques for distributed systems and communication protocols and protocol specification testing and verification (FORTE\/PSTV 1998) Paris Kluwer pp 457-467","DOI":"10.1007\/978-0-387-35394-4_28"},{"issue":"2","key":"p_5","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1006\/inco.1998.2706","article-title":"A formal approach to the integration of performance aspects in the modeling and analysis of concurrent systems","volume":"144","author":"Bernardo M","year":"1998","journal-title":"Inf Comput"},{"key":"p_6","first-page":"358","volume-title":"Degano P, Gorrieri R, Marchetti-Spaccamela A (eds) Automata, languages and programming, 24th international colloquium, vol 1256 of lecture notes in computer science, Bologna","author":"Ber M","year":"1997"},{"key":"p_8","volume-title":"Trace refinement of action systems. Reports on mathematics and computer science 153, \u00c4bo Akademi","author":"Bv R-J","year":"1994"},{"key":"p_9","volume-title":"Refinement calculus: a systematic introduction. Graduate texts in computer science","author":"Bv R-J","year":"1998"},{"key":"p_10","volume-title":"A discipline of programming","author":"Dij EW","year":"1976"},{"key":"p_11","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-58021-2_20","volume-title":"Haring G, Kotsis G (eds) Proceedings of the seventh international conference on modelling techniques and tools for computer performance evaluation, vol 794 of LNCS","author":"Gilmore S","year":"1994"},{"key":"p_13","volume-title":"Performance of computer communication systems: a model-based approach","author":"Hav BR","year":"1998"},{"key":"p_14","volume-title":"Refinement of dynamic systems. Technical report DSSE-TR-99-8","author":"Hallerstede S","year":"1999"},{"key":"p_15","unstructured":"[Heh] Hehner E Probabilistic predicative programming. Private communication"},{"key":"p_16","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","article-title":"Compositional performance modelling with the TIPPtool","volume":"39","author":"Hermanns H","year":"2000","journal-title":"Perform Eval"},{"key":"p_17","volume-title":"A compositional approach to performance modelling","author":"Hil J","year":"1996"},{"key":"p_18","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0166-5316(94)00038-7","article-title":"Performability modelling tools and techniques","volume":"25","author":"Haverkort BR","year":"1996","journal-title":"Perform Eval"},{"key":"p_19","volume-title":"Communicating sequential processes","author":"Hoa CAR","year":"1985"},{"key":"p_20","first-page":"71","volume-title":"Herzog U, Rettelbach M (eds) Proceedings of the second workshop on process algebra and performance modelling","author":"Hermanns H","year":"1994"},{"issue":"7","key":"p_21","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1093\/comjnl\/38.7.530","article-title":"Formal characterisation of immediate actions in SPA with nondeterministic branching","volume":"38","author":"Hermanns H","year":"1995","journal-title":"Comput J"},{"key":"p_22","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/BF01439850","article-title":"Specification techniques for markov reward models","volume":"3","author":"Haverkort BR","year":"1993","journal-title":"Discrete Event Dynamic Systems: Theory Application"},{"key":"p_23","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF01788563","article-title":"A state-based approach to communicating processes","volume":"3","author":"Jos MB","year":"1988","journal-title":"Distrib Comput"},{"issue":"2","key":"p_24","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","article-title":"Probabilistic models for the guarded command language","volume":"28","author":"Jifeng H","year":"1997","journal-title":"Sci Comput Program"},{"key":"p_25","volume-title":"Introduction to computer system performance evaluation","author":"Kan K","year":"1992"},{"key":"p_26","volume-title":"Finite markov chains. Undergraduate texts in mathematics","author":"Kemeny JG","year":"1976"},{"key":"p_27","volume-title":"Performance modelling with deterministic and stochastic petri nets","author":"Lin C","year":"1998"},{"key":"p_28","volume-title":"A class of generalized stochastic petri nets for the performance evaluation of multiprocessor systems. ACM trans comput syst 2:93-122","author":"Ajmone Marsan M","year":"1984"},{"key":"p_29","volume-title":"Communication and concurrency","author":"Mil R","year":"1989"},{"key":"p_30","volume-title":"Probabilistic modelling","author":"Mit I","year":"1998"},{"issue":"3","key":"p_31","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1145\/229542.229547","article-title":"Probabilistic predicate transformers","volume":"18","author":"Morgan C","year":"1996","journal-title":"ACM Trans Program Lang Syst"},{"key":"p_32","article-title":"Performance analysis using stochastic petri nets","author":"Mol MK","year":"1982","journal-title":"IEEE Trans Comput C-31(9):913-917"},{"key":"p_33","volume-title":"Probability, stochastic processes, and queueing theory: the mathematics of computer performance modelling","author":"Nel R","year":"1995"},{"key":"p_34","series-title":"Wiley series in probability and mathematical statistics","volume-title":"Markov decision processes-discrete stochastic dynamic programming","author":"Put ML","year":"1994"},{"key":"p_35","volume-title":"Petri nets. an introduction, vol 3 of EATCS monographs on theoretical computer science","author":"Rei W","year":"1985"},{"key":"p_36","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/0304-3975(94)00286-0","article-title":"Probabilistic communicating processes","volume":"152","author":"Sei K","year":"1995","journal-title":"Theor Comput Sci"},{"key":"p_37","series-title":"Wiley series in probability and statistics","volume-title":"Stochastic dynamic programming and the control of queueing systems","author":"Sen LI","year":"1999"},{"key":"p_38","volume-title":"Probabilistic imperative programming: a rigorous approach. Technical report","author":"Seidel K","year":"1997"},{"key":"p_39","volume-title":"Proceedings of the 8th nordic workshop on programming theory","author":"Sere K","year":"1996"},{"key":"p_40","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-2367-3","volume-title":"Performance and reliability analysis of computer systems: an example-based approach using the SHARPE software package","author":"Sahner R","year":"1996"},{"key":"p_41","series-title":"Wiley series in probability and mathematical statistics","volume-title":"Stochastic models: an algorithmic approach","author":"Tij HC","year":"1994"},{"key":"p_42","volume-title":"Proceedings of pacific rim international symposium on dependable computing","author":"Tro E","year":"1999"},{"key":"p_43","volume-title":"Using Z","author":"Woodcock J","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0037-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0037-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0037-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:45:27Z","timestamp":1641483927000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0037-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,11]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,11]]}},"alternative-id":["10.1007\/s00165-004-0037-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0037-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,11]]}}}