This HTML5 document contains 47 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n10http://localhost/temp/predkladatel/
n13http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n12http://linked.opendata.cz/resource/domain/vavai/projekt/
n19http://linked.opendata.cz/resource/domain/vavai/subjekt/
n18http://linked.opendata.cz/ontology/domain/vavai/
n17http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n4http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n7http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F12%3APU98150%21RIV13-GA0-26230___/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n15http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n9http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n11http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n5http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F12%3APU98150%21RIV13-GA0-26230___
rdf:type
n18:Vysledek skos:Concept
dcterms:description
This paper addresses the problem of conditional termination, which is that of defining the set of initial configurations from which a given program terminates. First we define the dual set, of initial configurations, from which a non-terminating execution exists, as the greatest fixpoint of the pre-image of the transition relation. This definition enables the representation of this set, whenever the closed form of the relation of the loop is definable in a logic that has quantifier elimination. This entails the decidability of the termination problem for such loops. Second, we present effective ways to compute the weakest precondition for non-termination for difference bounds and octagonal (non-deterministic) relations, by avoiding complex quantifier eliminations. We also investigate the existence of linear ranking functions for such loops. Finally, we study the class of linear affine relations and give a method of under-approximating the termination precondition for a non-trivial subclass This paper addresses the problem of conditional termination, which is that of defining the set of initial configurations from which a given program terminates. First we define the dual set, of initial configurations, from which a non-terminating execution exists, as the greatest fixpoint of the pre-image of the transition relation. This definition enables the representation of this set, whenever the closed form of the relation of the loop is definable in a logic that has quantifier elimination. This entails the decidability of the termination problem for such loops. Second, we present effective ways to compute the weakest precondition for non-termination for difference bounds and octagonal (non-deterministic) relations, by avoiding complex quantifier eliminations. We also investigate the existence of linear ranking functions for such loops. Finally, we study the class of linear affine relations and give a method of under-approximating the termination precondition for a non-trivial subclass
dcterms:title
Deciding Conditional Termination Deciding Conditional Termination
skos:prefLabel
Deciding Conditional Termination Deciding Conditional Termination
skos:notation
RIV/00216305:26230/12:PU98150!RIV13-GA0-26230___
n18:predkladatel
n19:orjk%3A26230
n4:aktivita
n9:Z n9:P
n4:aktivity
P(ED1.1.00/02.0070), P(GAP103/10/0306), P(GD102/09/H042), P(OC10009), Z(MSM0021630528)
n4:cisloPeriodika
7214
n4:dodaniDat
n5:2013
n4:domaciTvurceVysledku
n13:3600092
n4:druhVysledku
n16:J
n4:duvernostUdaju
n20:S
n4:entitaPredkladatele
n7:predkladatel
n4:idSjednocenehoVysledku
129752
n4:idVysledku
RIV/00216305:26230/12:PU98150
n4:jazykVysledku
n15:eng
n4:klicovaSlova
termination problem, conditional termination problem, difference bounds relations, octagonal relations, finite monoid affine relations
n4:klicoveSlovo
n14:difference%20bounds%20relations n14:termination%20problem n14:conditional%20termination%20problem n14:octagonal%20relations n14:finite%20monoid%20affine%20relations
n4:kodStatuVydavatele
DE - Spolková republika Německo
n4:kontrolniKodProRIV
[4B40A41E802E]
n4:nazevZdroje
Lecture Notes in Computer Science
n4:obor
n11:IN
n4:pocetDomacichTvurcuVysledku
1
n4:pocetTvurcuVysledku
3
n4:projekt
n12:GD102%2F09%2FH042 n12:GAP103%2F10%2F0306 n12:OC10009 n12:ED1.1.00%2F02.0070
n4:rokUplatneniVysledku
n5:2012
n4:svazekPeriodika
2012
n4:tvurceVysledku
Radu, Iosif Bozga, Marius Konečný, Filip
n4:zamer
n17:MSM0021630528
s:issn
0302-9743
s:numberOfPages
16
n10:organizacniJednotka
26230