Narrow Results

We present a technique based on the construction of finite automata to prove termination of string rewriting systems. Using this technique the tools Matchbox and TORPA are able to prove termination of particular string rewriting systems completely automatically for which termination was considered to be very hard until recently.

We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.

Verification of program termination is an important problem in program correctness analysis. Automatically proving termination or finding nonterminating inputs as counter-examples for many programs will be a big breakthrough in theoretical computer science. A remarkable result, provided by Tiwari(2004), showed that the termination of linear loops is decidable and an eventually nonterminating input can be found for the given nonterminating loop. But some essential lemmas were missing in that proof and his algorithm could not generate a nonterminating input, which might be more widely utilized in software testing. In this paper, we discuss these details carefully and present an algorithm for producing a nonterminating input automatically. We reduce the problem of finding a nonterminating input to that of computing real root bound of a multi-exponential polynomial. This algorithm has been implemented in a Maple package based on symbolic computation. Thereby a stronger and complete decidable result in termination problem is established.

Despite the extensive use of graphene-based materials in K-ion batteries, the effects of various edge morphologies of graphene on K atom adsorption and diffusion are unclear. In this study, the effects of K atom adsorption and diffusion on zigzag graphene nanoribbons (ZGNRs) with hydrogen (−H), ketone (=O), hydroxyl (−OH), and carboxyl (−COOH) terminal groups were investigated by density functional theory calculations. ZGNRs terminating with −H, =O and −COOH promote K atom adsorption, whereas those terminating with −OH suppress it. The −H, =O, −OH and −COOH terminations have a negligible effect on K atom diffusion in the inner region of ZGNRs. In the edge region, the diffusion barriers are nearly unchanged for −H and −OH terminations; however, they are increased for =O and −COOH terminations in the edge region compared to those in the inner region. All the terminal groups hinder K atom diffusion from the edge region toward the inner region. Our results suggest that −H termination enhances K atom adsorption and has a negligible effect on the diffusion barrier of K atom in the edge region. Therefore, the ZGNR with −H termination could be a promising candidate for K-ion batteries.

Multiway Decision Graphs (MDGs) have recently been proposed as an efficient representation for RTL designs. In this paper, we illustrate the MDG-based formal verification technique on the example of the Island Tunnel Controller. We investigate several techniques on how to deal with the nontermination problem of abstract state exploration, including a novel method based on retiming and circuit transformation. We provide comparative experimental results for the verification of a number of properties for the example using two well-known ROBDD-based verification tools, namely, SMV (Symbolic Model Verifier) and VIS (Verification Interacting with Synthesis), and we show the strength of the MDG approach to handling arbitrary data widths.

In the general context of presentations of monoids, we study normalization process that are determined by their restriction to length-two words. Garside’s greedy normal forms and quadratic convergent rewriting systems, in particular those associated with the plactic monoids, are typical examples. Having introduced a parameter, called the class and measuring the complexity of the normalization of length-three words, we analyze the normalization of longer words and describe a number of possible behaviors. We fully axiomatize normalizations of class $(4,3)$, show the convergence of the associated rewriting systems, and characterize those deriving from a Garside family.

This paper determines relations between two notions concerning monoids: factorability structure, introduced to simplify the bar complex; and quadratic normalization, introduced to generalize quadratic rewriting systems and normalizations arising from Garside families. Factorable monoids are characterized in the axiomatic setting of quadratic normalizations. Additionally, quadratic normalizations of class $\left(4,3\right)$ are characterized in terms of factorability structures and a condition ensuring the termination of the associated rewriting system.

Implantable cardioverter defibrillators (ICDs) have become standard therapy for many patients at risk for reentrant ventricular tachycardias. By applying one or more series of suprathreshold stimuli, the antitachycardia pacing modality of ICDs successfully terminates ventricular tachycardia in up to 90% of attempted trials. However, many aspects of why antitachycardia pacing is successful are unknown. We conducted numerical simulations to investigate the dynamics of reentry termination, and have in particular studied situations where (1) the stimulus site is located at some distance away from the reentrant loop, and (2) the reentrant circuit is sufficiently short that a period-doubling bifurcation to repolarization alternans has occurred. Our study shows that when applying a single stimulus, termination of reentry is possible only when the stimulus site is very close to the reentrant loop. However, during alternans, termination is much facilitated by the presence of spatial gradients in action potential duration and recovery time.