Advertisement

Equations Over Finite State Machines

  • Tiziano Villa
  • Nina Yevtushenko
  • Robert K. Brayton
  • Alan Mishchenko
  • Alexandre Petrenko
  • Alberto Sangiovanni-Vincentelli
Chapter

Abstract

A finite state machine (FSM) is a 5-tuple M = ⟨S, I, O, T, r⟩ where S represents the finite state space, I represents the finite input space, O represents the finite output space and TI ×S ×S ×O is the transition relation. On input i, the FSM at present state p may transit to next state n and produce output o iff (i, p, n, o) ∈ T. State rS represents the initial or reset state. We denote the projection of relation T to I ×S ×S (next state relation) by T n I ×S ×S, i.e., (i, s, s′) ∈ T n ⇔ ∃o (i, s, s′, o) ∈ T; similarly, we denote the projection of relation T to I ×S ×O (output relation) by T o I ×S ×O, i.e., (i, s, o) ∈ T o ⇔ ∃s′ (i, s, s′, o) ∈ T. Sometimes δ is used instead of T n and λ instead of T o .

Keywords

Composition Operator Finite State Machine Regular Language Outgoing Edge Parallel Composition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  • Tiziano Villa
    • 1
  • Nina Yevtushenko
    • 2
  • Robert K. Brayton
    • 3
  • Alan Mishchenko
    • 4
  • Alexandre Petrenko
    • 5
  • Alberto Sangiovanni-Vincentelli
    • 4
  1. 1.Dipartimento D’InformaticaUniversità di VeronaVeronaItaly
  2. 2.Department of EECSTomsk State UniversityTomskRussia
  3. 3.Department of Electrical Engineering and Computer ScienceUniversity of CaliforniaBerkeleyUSA
  4. 4.Department of Electrical Engineering and Computer Science (EECS)University of California, BerkeleyBerkeleyUSA
  5. 5.Computer Research Institute of Montreal (CRIM)MontrealCanada

Personalised recommendations