Informační systém MU
KUČERA, Antonín a Javier ESPARZA. A Logical Viewpoint on Process-algebraic Quotients. Journal of logic and computation. Oxford: Oxford University Press, 2003, roč. 13, č. 6, s. 863-880. ISSN 0955-792X.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název A Logical Viewpoint on Process-algebraic Quotients
Autoři KUČERA, Antonín (203 Česká republika, garant) a Javier ESPARZA (724 Španělsko).
Vydání Journal of logic and computation, Oxford, Oxford University Press, 2003, 0955-792X.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Velká Británie a Severní Irsko
Utajení není předmětem státního či obchodního tajemství
Impakt faktor Impact factor: 0.586
Kód RIV RIV/00216224:14330/03:00008439
Organizační jednotka Fakulta informatiky
UT WoS 000187988100004
Klíčová slova anglicky transition systems; behavioural equivalences; quotients
Štítky behavioural equivalences, quotients, transition systems
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 22. 11. 2006 18:19.
Anotace
Let E be a process equivalence. A formula F is preserved by E-quotients iff for every process S of a transition system T we have that if S satisfies F, then also [S] satisfies F, where [S] is the equivalence class of S in the quotient of T under E. We classify all formulae of Hennessy-Milner logic which are preserved by E-quotients of image-finite processes. Our result is generic in the sense that it works for a large class of process equivalences which admit a modal characterization in Hennessy-Milner logic satisfying certain closure properties. A practical applicability of the result is demonstrated on equivalences of the linear/branching time spectrum.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM 143300001, záměrNázev: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů
Zobrazeno: 14. 5. 2024 01:22