کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6874868 | 1441445 | 2018 | 33 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
ULTraS at work: Compositionality metaresults for bisimulation and trace semantics
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: ULTraS at work: Compositionality metaresults for bisimulation and trace semantics ULTraS at work: Compositionality metaresults for bisimulation and trace semantics](/preview/png/6874868.png)
چکیده انگلیسی
The ULTraS metamodel can be instantiated to a large number of well established models, including labeled transition systems together with their probabilistic, deterministic timed, and stochastic timed extensions. Several metaequivalences have been defined on the ULTraS metamodel, which can be instantiated to well known behavioral equivalences for those specific models. However, new equivalences pop up, instead of the widely accepted ones, in the case of processes featuring probabilities and internal nondeterminism. Most importantly, the properties of the metaequivalences have not been investigated yet. Focusing on bisimulation and trace semantics, we first show that, by simply introducing the notion of resolution in the ULTraS theory, and exchanging the order of certain universal quantifiers in the definition of the metaequivalences, it is possible to retrieve the behavioral equivalences not captured before, as well as to keep the new ones. We then study the compositionality, with respect to typical process algebraic operators, of the two bisimulation metaequivalences and of the two trace metaequivalences respectively arising from the two different quantification orders. The congruence metaresults for parallel composition confirm the existence of a foundational difference in the compositionality of bisimulation and trace semantics when internal nondeterminism is present, which had recently emerged in the specific setting of probabilistic and nondeterministic processes.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 94, January 2018, Pages 150-182
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 94, January 2018, Pages 150-182
نویسندگان
Marco Bernardo,