Detail publikace

Deciding Conditional Termination

KONEČNÝ Filip, IOSIF Radu a BOZGA Marius. Deciding Conditional Termination. Lecture Notes in Computer Science, roč. 2012, č. 7214, s. 252-266. ISSN 0302-9743.
Název česky
Rozhodování podmíněné konečnosti
Typ
článek v časopise
Jazyk
angličtina
Autoři
Konečný Filip, Ing. (UITS FIT VUT)
Iosif Radu (VERIMAG)
Bozga Marius (VERIMAG)
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
Vydavatel
Springer Verlag
BibTeX 
@ARTICLE{FITPUB9986,
   author = "Filip Kone\v{c}n\'{y} and Radu Iosif and Marius Bozga",
   title = "Deciding Conditional Termination",
   pages = "252--266",
   journal = "Lecture Notes in Computer Science",
   volume = 2012,
   number = 7214,
   year = 2012,
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9986"
}
Nahoru