• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

On the Model Checking of Finite State Transducers over Semigroups

Gnatenko A., Zakharov V.

The syntax and semantics of the new temporal logic LP-CTL * designed for the formal specification of the behavior of sequential responsive programs, modeled by automata-transducers (transducers) over semigroups, are developed. An algorithm is developed for verifying the feasibility of the formulas of the proposed temporal logic on models represented by finite transducers working on free semigroups. The correctness of the developed algorithm is proved and an upper bound of its complexity is obtained.