Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Consistency checking of automata functional specifications

  • Conference paper
  • First Online:
Logic Programming and Automated Reasoning (LPAR 1993)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 698))

Abstract

The use of a subset of a first order unary predicate language as a language for deterministic cyclic automata specification is considered. The formulas of the language are interpreted over the set of integers, which is regarded as a discrete time domain. An efficient algorithm for consistency checking of specifications in this language, based on modified resolution procedure, is suggested. This algorithm is implemented as a completion procedure. The use of the integers as the interpretation domain for the specification language made it possible to essentially simplify this procedure.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Church: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Inst. for Symbolic Logic, Cornell University, Ithaca, New York: 1957, pp. 3–50

    Google Scholar 

  2. J.R. Buchi: Weak second-order arithmetic and finite automata. Zeitshr. Math. Logik und Grundl. der Math. 6, 66–92 (1960)

    Google Scholar 

  3. B.A. Trakhtenbrot, J.M. Barzdin: Finite automata (behaviour and synthesis) (in Russian). Moscow, USSR: Nauka 1970

    Google Scholar 

  4. B. Auernheimer, R.A. Kemmerer: RT-ASLAN: A specification language for real-time systems. IEEE Transactions on Software Engineering SE-12, 879–889 (1986)

    Google Scholar 

  5. F. Jahanian, A. Ka-Lan-Hok: Safety analysis of timing properties in realtime systems. IEEE Transactions on Software Engineering SE-12, 890–904 (1986)

    Google Scholar 

  6. C. Ghezzi, D. Handrioli, A. Morzenti: TRIO: A logic language for executable specifications of real-time systems. Journal of Systems and Software 12, 107–123 (1990)

    Article  Google Scholar 

  7. A.N. Chebotarev: On one approach to functional specification of automata systems. Cybernetics and Systems Analysis (Translated from Russian), to be appeared, 1993

    Google Scholar 

  8. C.L. Chang, R.C.T. Lee: Symbolic logic and mechanical theorem proving. New York-San Francisco-London: Academic press 1973

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Glushkov Institute of Cybernetics, Ukrainian Academy of Sciences, Glushkov prosp., 40, 252207, Kiev, Ukraine

    Anatoli N. Chebotarev & Marina K. Morokhovets

Authors
  1. Anatoli N. Chebotarev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marina K. Morokhovets
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chebotarev, A.N., Morokhovets, M.K. (1993). Consistency checking of automata functional specifications. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1993. Lecture Notes in Computer Science, vol 698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56944-8_43

Download citation

  • DOI: https://doi.org/10.1007/3-540-56944-8_43

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56944-2

  • Online ISBN: 978-3-540-47830-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation