Detail publikace

Deciding Conditional Termination

KONEČNÝ, F.; IOSIF, R.; BOZGA, M. Deciding Conditional Termination. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 252-266. ISSN: 0302-9743.
Název česky
Rozhodování podmíněné konečnosti
Typ
článek v časopise
Jazyk
anglicky
Autoři
Konečný Filip, Ing., Ph.D.
Radu Iosif
Bozga Marius
Klíčová slova

termination problem, conditional termination problem, difference bounds relations, octagonal relations, finite monoid affine relations

Abstrakt

Tento článek se zabývá problémem podmíněné konečnosti -- problémem definování množiny počátečních konfigurací, z nichž jsou všechny běhy programu konečné. Nejdříve definujeme duální množinu počátečních konfigurací, z nichž existují nekonečné běhy, jako největší pevný bod inverzního obrazu přechodové funkce. Tato definice umožňuje reprezentovat tuto množinu tehdy, když lze uzavřený tvar relace cyklu programu definovat v logice, ve které je možná eliminace kvantifikátorů. Z toho vyplývá, že problém konečnosti je pro takové smyčky rozhodnutelný. Dále představujeme efektivní metody výpočtu nejobecnějších vstupních podmínek pro nekonečnost pro oktagonální (nedeterministicné) relace, bez nutnosti eliminace kvantifikátorů. Také pro tuto třídu studujeme existenci lineárních hodnotících funkcí. Nakonec studujeme třídu lineárních afinních relací a prezentujeme metodu pro výpočet pod-aproximací vstupních podmínek pro konečnost pro netriviální podtřídu afinních relací. Provedli jsme několik experimentů a obdrželi slibné výsledky.

Rok
2012
Strany
252–266
Časopis
Lecture Notes in Computer Science, roč. 2012, č. 7214, ISSN 0302-9743
BibTeX 
@article{BUT91442,
  author="Filip {Konečný} and Iosif {Radu} and Marius {Bozga}",
  title="Deciding Conditional Termination",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7214",
  pages="252--266",
  issn="0302-9743"
}
Nahoru