DP lower bounds for equivalence-checking and model-checking of one-counter automata

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Fakultu sportovních studií, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky DP dolní složitostní odhady pro problémy související s formální verifikací automatů s jedním čítačem
Autoři

JANČAR Petr KUČERA Antonín MOLLER Faron SAWA Zdeněk

Rok publikování 2004
Druh Článek v odborném periodiku
Časopis / Zdroj Information and Computation
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova one-counter automata; equivalence-checking; bisimilarity
Popis Je podána obecná metoda pro dokazování DP dolního složitostního odhadu pro problémy související s formální verifikací automatů s jedním čítačem. Za tímto účelem je prezentována redukce problému SAT-UNSAT na problém platnosti formulí vhodného fragmentu Presburgerovy aritmetiky. Tento fragment obsahuje pouze formule s jednou volnou proměnnou a je velmi vhodný pro redukci na problém simulačních ekvivalencí mezi procesy automatů s jedním čítačem. Tímto způsobem je prokázána DP-těžkost libovolné ekvivalence mezi simulační a bisimulační ekvivalencí. Je také dokázána DP-těžkost problému ověřování platnosti formulí temporální logiky EF.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info