<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.3 20210610//EN" "https://jats.nlm.nih.gov/publishing/1.3/JATS-journalpublishing1-3.dtd">
<article article-type="review-article" dtd-version="1.3" xml:lang="en">
  <front>
    <journal-meta>
      <journal-title-group>
        <journal-title>Computing, Telecommunication and Control</journal-title>
        <trans-title-group xml:lang="ru">
          <trans-title>Информатика, телекоммуникации и управление</trans-title>
        </trans-title-group>
      </journal-title-group>
      <issn pub-type="epub">2687-0517</issn>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="publisher-id">8</article-id>
      <article-id pub-id-type="doi">10.5862/JCSTCS.236.9</article-id>
      <title-group>
        <article-title>Survey on Formal Methods in Robotics</article-title>
        <trans-title-group xml:lang="ru">
          <trans-title>Обзор применения формальных методов в робототехнике</trans-title>
        </trans-title-group>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <name>
            <surname>Mordvinov</surname>
            <given-names>Dmitrii</given-names>
          </name>
          <email>mordvinov.dmitry@gmail.com</email>
        </contrib>
        <contrib contrib-type="author">
          <name>
            <surname>Litvinov</surname>
            <given-names>Yury</given-names>
          </name>
        </contrib>
      </contrib-group>
      <pub-date publication-format="electronic" date-type="pub" iso-8601-date="2016-03-31">
        <day>31</day>
        <month>03</month>
        <year>2016</year>
      </pub-date>
      <issue>1</issue>
      <issue-id pub-id-type="publisher-id">236</issue-id>
      <fpage>84</fpage>
      <lpage>107</lpage>
      <abstract xml:lang="en">
        <p>This paper is a survey of applying formal methods in the robotics field. We consider a number of recent works on robotic behavior specification in terms of temporal logics and using the model checking approach. Formal analysis techniques for Petri nets and robotics systems modeling using those methods are also considered. Verification of hybrid systems, application of process algebras for concurrent systems and other approaches for synthesis and verification of robotics controllers are described. We survey both fundamental papers that lay a foundation for the entire branches of research and recent papers from the top conferences of the last five years hoping to cover most of the actively developed research topics.</p>
      </abstract>
      <kwd-group xml:lang="en">
        <kwd>formal methods</kwd>
        <kwd>robotics</kwd>
        <kwd>temporal logics</kwd>
        <kwd>formal verification</kwd>
        <kwd>synthesis of formal systems</kwd>
      </kwd-group>
    </article-meta>
  </front>
</article>
