اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدAlgebraic Structure of Combined Traces
45
0
0.0
(
0
)
تأليف
Lukasz Mikulski
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Traces and their extension called combined traces (comtraces) are two formal models used in the analysis and verification of concurrent systems. Both models are based on concepts originating in the theory of formal languages, and they are able to capture the notions of causality and simultaneity of atomic actions which take place during the process of a systems operation. The aim of this paper is a transfer to the domain of comtraces and developing of some fundamental notions, which proved to be successful in the theory of traces. In particular, we introduce and then apply the notion of indivisible steps, the lexicographical canonical form of comtraces, as well as the representation of a comtrace utilising its linear projections to binary action subalphabets. We also provide two algorithms related to the new notions. Using them, one can solve, in an efficient way, the problem of step sequence equivalence in the context of comtraces. One may view our results as a first step towards the development of infinite combined traces, as well as recognisable languages of combined traces.
قيم البحث
اقرأ أيضاً
In the theory of coalgebras, trace semantics can be defined in various distinct ways, including through algebraic logics, the Kleisli category of a monad or its Eilenberg-Moore category. This paper elaborates two new unifying ideas: 1) coalgebraic tr
ace semantics is naturally presented in terms of corecursive algebras, and 2) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof, and allows to derive conditions under which some of them coincide.
89 -
Desharnais Jules (Departement dinformatique et de genie logiciel
, n Universite Laval
, Quebec
2010
Five algebraic notions of termination are formalised, analysed and compared: wellfoundedness or Noetherity, Lobs formula, absence of infinite iteration, absence of divergence and normalisation. The study is based on modal semirings, which are additiv
ely idempotent semirings with forward and backward modal operators. To model infinite behaviours, idempotent semirings are extended to divergence semirings, divergence Kleene algebras and omega algebras. The resulting notions and techniques are used in calculational proofs of classical theorems of rewriting theory. These applications show that modal semirings are powerful tools for reasoning algebraically about the finite and infinite dynamics of programs and transition systems.
This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 Algebraic effect handlers go mainstream. It is targeted roughly at the level of a d
octoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts who would like to know what they have to do with algebra. We draw an uninterrupted line of thought between algebra and computational effects. We begin on the mathematical side of things, by reviewing the classic notions of universal algebra: signatures, algebraic theories, and their models. We then generalize and adapt the theory so that it applies to computational effects. In the last step we replace traditional mathematical notation with one that is closer to programming languages.
In this paper, we settle a problem in probabilistic verification of infinite--state process (specifically, {it probabilistic pushdown process}). We show that model checking {it stateless probabilistic pushdown process} (pBPA) against {it probabilistic computational tree logic} (PCTL) is undecidable.
In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown modu
le-checking for CTL. On the other hand, we show that ATL* module-checking of PMS turns out to be 4EXPTIME-complete, hence exponentially harder than both CTL* pushdown module-checking and ATL* model-checking of PMS. Our result for ATL* provides a rare example of a natural decision problem that is elementary yet but with a complexity that is higher than triply exponential-time.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
