ترغب بنشر مسار تعليمي؟ اضغط هنا

Non-Termination Sets of Simple Linear Loops

110   0   0.0 ( 0 )
 نشر من قبل Dai Liyun
 تاريخ النشر 2012
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English




اسأل ChatGPT حول البحث

A simple linear loop is a simple while loop with linear assignments and linear loop guards. If a simple linear loop has only two program variables, we give a complete algorithm for computing the set of all the inputs on which the loop does not terminate. For the case of more program variables, we show that the non-termination set cannot be described by Tarski formulae in general



قيم البحث

اقرأ أيضاً

We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient language to express non-termination. Of course, such property is generally undecidable. However, by restricting the language to known decidable cases, we exhibit new classes of loops, the non-termination of which is decidable. We present a bunch of examples.
Five algebraic notions of termination are formalised, analysed and compared: wellfoundedness or Noetherity, Lobs formula, absence of infinite iteration, absence of divergence and normalisation. The study is based on modal semirings, which are additiv ely idempotent semirings with forward and backward modal operators. To model infinite behaviours, idempotent semirings are extended to divergence semirings, divergence Kleene algebras and omega algebras. The resulting notions and techniques are used in calculational proofs of classical theorems of rewriting theory. These applications show that modal semirings are powerful tools for reasoning algebraically about the finite and infinite dynamics of programs and transition systems.
We present an efficient approach to prove termination of monotone programs with integer variables, an expressive class of loops that is often encountered in computer programs. Our approach is based on a lightweight static analysis method and takes ad vantage of simple %nice properties of monotone functions. Our preliminary implementation %beats shows that our tool has an advantage over existing tools and can prove termination for a high percentage of loops for a class of benchmarks.
106 - Vincent Danos 2010
We present a reduction of the termination problem for a Turing machine (in the simplified form of the Post correspondence problem) to the problem of determining whether a continuous-time Markov chain presented as a set of Kappa graph-rewriting rules has an equilibrium. It follows that the problem of whether a computable CTMC is dissipative (ie does not have an equilibrium) is undecidable.
We consider agents with non-linear preferences given by private values and private budgets. We quantify the extent to which posted pricing approximately optimizes welfare and revenue for a single agent. We give a reduction framework that extends the approximation of multi-agent pricing-based mechanisms from linear utility to nonlinear utility. This reduction framework is broadly applicable as Alaei et al. (2012) have shown that mechanisms for linear agents can generally be interpreted as pricing-based mechanisms. We give example applications of the framework to oblivious posted pricing (e.g., Chawla et al., 2010), sequential posted pricing (e.g., Yan, 2011), and virtual surplus maximization (Myerson, 1981).
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا