Články v časopisech
| Konečný, F., Iosif, R., Bozga, M.: Deciding Conditional Termination, In: Lecture Notes in Computer Science, roč. 2012, č. 7214, DE, s. 252-266, ISSN 0302-9743 | | Jazyk publikace: | angličtina |
|---|
| Název publikace: | Deciding Conditional Termination |
|---|
| Název (cs): | Rozhodování podmíněné konečnosti |
|---|
| Strany: | 252-266 |
|---|
| Místo vydání: | DE |
|---|
| Rok: | 2012 |
|---|
| Časopis: | Lecture Notes in Computer Science, roč. 2012, č. 7214, DE |
|---|
| ISSN: | 0302-9743 |
|---|
| Klíčová slova |
|---|
| termination problem, conditional termination problem, difference bounds relations, octagonal relations, finite monoid affine relations |
| Anotace |
|---|
| 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. |
| BibTeX: |
|---|
@ARTICLE{
author = {Filip Konečný 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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=9986}
} |
|
Fakulta informačních technologií
![[dnssec]](/common/img/dnssec.png)