Fulltext

Don't care words with an application totheautomata-based approach for real addition

Eisinger, Jochen ; Klaedtke, Felix

In: Formal Methods in System Design, 2008, vol. 33, no. 1-3, p. 85-115

Ajouter à la liste personnelle
    Titre
    • Don't care words with an application totheautomata-based approach for real addition
    Auteur
    • Eisinger, Jochen. Department of Computer Science, Albert-Ludwigs-Universität Freiburg, Georges-Köhler-Allee 051, 79110, Freiburg, Germany
    • Klaedtke, Felix. Computer Science Department, ETH Zurich, Haldeneggsteig 4, IFW C 47.2, 8092, Zurich, Switzerland
    Type de document
    • Postprint
    Langue
    • Anglais
    Publié dans
    • Formal Methods in System Design, 2008, vol. 33, no. 1-3, p. 85-115. Springer US; http://www.springer-ny.com
    Autre version électronique
    Identifiant OAI-PMH
    • oai:doc.rero.ch:316989
    Summary
    Automata have proved to be a useful tool in infinite-state model checking, since they can represent infinite sets of integers and reals. However, analogous to the use of binary decision diagrams (bdds) to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation. In this article, we generalize the notion of "don't cares” for bdds to word languages as a means to reduce the automata sizes. We show that the minimal weak deterministic Büchi automaton (wdba) with respect to a given don't care set, under certain restrictions, is uniquely determined and can be efficiently constructed. We apply don't cares to improve the efficiency of a decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on wdbas