On the model checking of finite state transducers over semigroups

On the model checking of finite state transducers over semigroups

Автор: Gnatenko A.R., Zakharov V.A.

Журнал: Труды Института системного программирования РАН @trudy-isp-ran

Статья в выпуске: 3 т.30, 2018 года.

Бесплатный доступ

Sequential reactive systems represent programs that interact with the environment by receiving signals or requests and react to these requests by performing operations with data. Such systems simulate various software like computer drivers, real-time systems, control procedures, online protocols etc. In this paper, we study the verification problem for the programs of this kind. We use finite state transducers over semigroups as formal models of reactive systems. We introduce a new specification language LP-CTL* to describe the behavior of transducers. This language is based on the well-known temporal logic CTL* and has two distinguished features: 1) each temporal operator is parameterized with a regular expression over input alphabet of the transducer, and 2) each atomic proposition is specified by a regular expression over the output alphabet of the transducer. We develop a tabular algorithm for model checking of finite state transducers over semigroups against LP-CTL* formulae, prove its correctness, and estimate its complexity. We also consider a special fragment of LP-CTL* language, where temporal operators are parameterized with regular expressions over one-letter alphabet, and show that this fragment may be used to specify usual Kripke structures, while it is more expressive than usual CTL*.

Еще

Reactive program, transducer, verification, model checking, temporal logic, finite state automaton, regular language

Короткий адрес: https://sciup.org/14916546

IDR: 14916546   |   DOI: 10.15514/ISPRAS-2018-30(3)-21

Список литературы On the model checking of finite state transducers over semigroups

  • Alur R., Cerny P. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of 38-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2011, pp. 599-610
  • Alur R., Moarref S., and Topcu U. Pattern-based refinement of assume-guarantee specifications in reactive synthesis. In Proceedings of 21-st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2015, pp. 501-516.
  • Baier C., Katoen J. Principles of Model Checking, 2008, MIT Press.
  • Blattner M., Head T. The decidability of equivalence for deterministic finite transducers. Journal of Computer and System Sciences, 1979, vol. 1, pp. 45-49.
  • Blattner M., T. Head T. Single-valued a-transducers. Journal of Computer and System Sciences, vol. 15, 1977, pp. 310-327.
  • Culik K, Karhumaki J. The equivalence of finite-valued transducers (on HDTOL languages) is decidable. Theoretical Computer Science, 1986, vol. 47, pp. 71-84.
  • Bouajjani A., Jonsson B., Nilsson M., Touili T. Regular Model Checking. Proceedings of 12-th International Conference on Computer Aided Verification, 2000, p. 403-418.
  • Clarke (Jr.) E. M., Grumberg O., Peled D. A. Model Checking. MIT Press, 1999.
  • Diekert V., Rozenberg G. eds. The Book of Traces, 1995, World Scientific, Singapore.
  • Emerson E.A., Halpern J.Y. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, vol. 30, N 1, 1985, pp. 1-24.
  • Etessami K., WilkeT. An Until Hierarchy and Other Applications of and Ehrenfeucht-Fraisse Game for Temporal Logic. Information and Computation, vol. 160, 2000, pp. 88-108.
  • Gnatenko A.R., Zakharov V. A. On the complexity of verification of finite state machines over commutative semigroups. In Proceedings of the 18-th International Conference "Problems of Theoretical Cybernetics'', 2017, pp. 68-70.
  • Griffiths T. The unsolvability of the equivalence problem for free nondeterministic generalized machines. Journal of the ACM, vol. 15, 1968, pp. 409-413.
  • Henriksen J. G., Thiagarajan P.S. Dynamic linear time temporal logic. Annals of Pure and Applied Logic, vol. 96, 1999, pp.187-207.
  • Hu Q., D'Antoni L. Automatic Program Inversion using Symbolic Transducers. In Proceedings of the 38-th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, pp. 376-389.
  • Ibarra O. The unsolvability of the equivalence problem for Efree NGSM’s with unary input (output) alphabet and applications. SIAM Journal on Computing, vol. 4, 1978, pp. 524-532.
  • Kozlova D. G., Zakharov V. A. On the model checking of sequential reactive systems. Proceedings of the25-th International Workshop on Concurrency, Specification and Programming (CS&P 2016), CEUR Workshop Proceedings, vol. 1698, 2016, pp. 233-244.
  • Kupferman O., Piterman N., Vardi M.Y. Extended Temporal Logic Revisited. In Proceedings of 12-th International Conference on Concurrency Theory, 2001, pp. 519-535.
  • Schutzenberger M. P. Sur les relations rationnelles. In Proceedings of Conference on Automata Theory and Formal Languages, 1975, pp. 209-213.
  • Sakarovitch J., de Souza R. On the decomposition of k-valued rational relations. In Proceedings of 25-th International Symposium on Theoretical Aspects of Computer Science, 2008, pp. 621-632.
  • Sakarovitch J., de Souza R. On the decidability of bounded valuedness for transducers. In Proceedings of the 33-rd International Symposium on Mathematical Foundations of Computer Science, 2008, pp. 588-600.
  • De Souza R. On the decidability of the equivalence for k-valued transducers. In Proceedings of 12-th International Conference on Developments in Language Theory, 2008, pp. 252-263.
  • Thakkar J., Kanade A., Alur R. A transducer-based algorithmic verification of retransmission protocols over noisy channels. In Proceedings of IFIP Joint International Conference on Formal Techniques for Distributed Systems, 2013, pp. 209-224.
  • Vardi M.Y., Wolper P. Yet Another Process Logic. Logic of Programs, 1983, pp. 501-512.
  • Veanes M., Hooimeijer P., Livshits B. et al. Symbolic finite state transducers: algorithms and applications. In Proceedings of the 39-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, vol. 147, 2012, pp. 137-150.
  • Weber A. Decomposing finite-valued transducers and deciding their equivalence. SIAM Journal on Computing. vol. 22, 1993, pp. 175-202.
  • Wolper P. Temporal Logic Can Be More Expressive. Information and Control, vol. 56, N 1/2, 1983, pp. 72-99.
  • Wolper P., Boigelot B. Verifying systems with infinite but regular state spaces. In Proceedings of the 10-th Int. Conf. on Computer Aided Verification (CAV-1998), 1998, pp. 88-97.
  • Zakharov V.A. Equivalence checking problem for finite state transducers over semigroups. In Proceedings of the~6-th International Conference on Algebraic Informatics (CAI-2015), 2015, pp. 208-221.
Еще
Статья научная
SciUp 2024 © 2024 ©