Using SAT for Combinational Implementation Checking

The problem of checking whether a system of incompletely specified Boolean functions is implemented by the given combinational circuit is considered. The task is reduced to testing out if two given logical descriptions are equivalent on the domain of one of them having functional indeterminacy. We present a novel SAT-based verification method that is used for testing whether the given circuit satisfies all the conditions represented by the system of incompletely specified Boolean functions.

Detection of foveation windows and analysis of foveation sequences in congenital nystagmus

Congenital nystagmus (CN) is an ocular-motor disorder characterised by involuntary, conjugated ocular oscillations, that can arise since the first months of life. Pathogenesis of congenital nystagmus is still under investigation. In general, CN patients show a considerable decrease of their visual acuity: image fixation on the retina is disturbed by nystagmus continuous oscillations, mainly horizontal. However, image stabilisation is still achieved during the short periods in which eye velocity slows down while the target image is placed onto the fovea (called foveation intervals). To quantify the extent of nystagmus, eye movement recording are routinely employed, allowing physicians to extract and analyse nystagmus main features such as shape, amplitude and frequency. Using eye movement recording, it is also possible to compute estimated visual acuity predictors: analytical functions which estimates expected visual acuity using signal features such as foveation time and foveation position variability. Use of those functions add information to typical visual acuity measurement (e.g. Landolt C test) and could be a support for therapy planning or monitoring. This study focus on robust detection of CN patients' foveations. Specifically, it proposes a method to recognize the exact signal tracts in which a subject foveates, This paper also analyses foveation sequences. About 50 eyemovement recordings, either infrared-oculographic or electrooculographic, from different CN subjects were acquired. Results suggest that an exponential interpolation for the slow phases of nystagmus could improve foveation time computing and reduce influence of breaking saccades and data noise. Moreover a concise description of foveation sequence variability can be achieved using non-fitting splines. © 2009 Springer Berlin Heidelberg.

Sequences of Maximal Degree Vertices in Graphs

2000 Mathematics Subject Classification: 05C35.

Verification of Procedural Programs via Building their Generalized Nets Models

Магдалина Василева Тодорова - В статията е описан подход за верификация на процедурни програми чрез изграждане на техни модели, дефинирани чрез обобщени мрежи. Подходът интегрира концепцията “design by contract” с подходи за верификация от тип доказателство на теореми и проверка на съгласуваност на модели. За целта разделно се верифицират функциите, които изграждат програмата относно спецификации според предназначението им. Изгражда се обобщен мрежов модел, специфициащ връзките между функциите във вид на коректни редици от извиквания. За главната функция на програмата се построява обобщен мрежов модел и се проверява дали той съответства на мрежовия модел на връзките между функциите на програмата. Всяка от функциите на програмата, която използва други функции се верифицира и относно спецификацията, зададена чрез мрежовия модел на връзките между функциите на програмата.

Approximate Model Checking of Real-Time Systems for Linear Duration Invariants

Real-time systems are usually modelled with timed automata and real-time requirements relating to the state durations of the system are often specifiable using Linear Duration Invariants, which is a decidable subclass of Duration Calculus formulas. Various algorithms have been developed to check timed automata or real-time automata for linear duration invariants, but each needs complicated preprocessing and exponential calculation. To the best of our knowledge, these algorithms have not been implemented. In this paper, we present an approximate model checking technique based on a genetic algorithm to check real-time automata for linear durration invariants in reasonable times. Genetic algorithm is a good optimization method when a problem needs massive computation and it works particularly well in our case because the fitness function which is derived from the linear duration invariant is linear. ACM Computing Classification System (1998): D.2.4, C.3.

Topic Segmentation: How Much Can We Do by Counting Words and Sequences of Words

In this paper, we present an innovative topic segmentation system based on a new informative similarity measure that takes into account word co-occurrence in order to avoid the accessibility to existing linguistic resources such as electronic dictionaries or lexico-semantic databases such as thesauri or ontology. Topic segmentation is the task of breaking documents into topically coherent multi-paragraph subparts. Topic segmentation has extensively been used in information retrieval and text summarization. In particular, our architecture proposes a language-independent topic segmentation system that solves three main problems evidenced by previous research: systems based uniquely on lexical repetition that show reliability problems, systems based on lexical cohesion using existing linguistic resources that are usually available only for dominating languages and as a consequence do not apply to less favored languages and finally systems that need previously existing harvesting training data. For that purpose, we only use statistics on words and sequences of words based on a set of texts. This solution provides a flexible solution that may narrow the gap between dominating languages and less favored languages thus allowing equivalent access to information.

On a Theorem by Van Vleck Regarding Sturm Sequences

In 1900 E. B. Van Vleck proposed a very efficient method to compute the Sturm sequence of a polynomial p (x) ∈ Z[x] by triangularizing one of Sylvester’s matrices of p (x) and its derivative p′(x). That method works fine only for the case of complete sequences provided no pivots take place. In 1917, A. J. Pell and R. L. Gordon pointed out this “weakness” in Van Vleck’s theorem, rectified it but did not extend his method, so that it also works in the cases of: (a) complete Sturm sequences with pivot, and (b) incomplete Sturm sequences. Despite its importance, the Pell-Gordon Theorem for polynomials in Q[x] has been totally forgotten and, to our knowledge, it is referenced by us for the first time in the literature. In this paper we go over Van Vleck’s theorem and method, modify slightly the formula of the Pell-Gordon Theorem and present a general triangularization method, called the VanVleck-Pell-Gordon method, that correctly computes in Z[x] polynomial Sturm sequences, both complete and incomplete.

Sturm Sequences and Modified Subresultant Polynomial Remainder Sequences

ACM Computing Classification System (1998): F.2.1, G.1.5, I.1.2.