Document Open Access Logo

The Siren Song of Temporal Synthesis (Invited Talk)

Author Moshe Y. Vardi



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.1.pdf
  • Filesize: 253 kB
  • 1 pages

Document Identifiers

Author Details

Moshe Y. Vardi
  • Department of Computer Science, Rice University, Houston, TX, USA

Cite AsGet BibTex

Moshe Y. Vardi. The Siren Song of Temporal Synthesis (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, p. 1:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.1

Abstract

One of the most significant developments in the area of design verification over the last three decade is the development of algorithmic methods for verifying temporal specification of finite-state designs. A frequent criticism against this approach, however, is that verification is done after significant resources have already been invested in the development of the design. Since designs invariably contains errors, verification simply becomes part of the debugging process. The critics argue that the desired goal is to use temporal specification in the design development process in order to guarantee the development of correct designs. This is called temporal synthesis. In this talk I will review 60 years of research on the temporal synthesis problem, describe the automata-theoretic approach developed to solve this problem, and describe both successes and failures of this research program [Zhu et al., 2017a and 2017b].

Subject Classification

ACM Subject Classification
  • Software and its engineering
Keywords
  • Formal Methods
  • Temporal Synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. A symbolic approach to safety LTL synthesis. In Proc. 13th Int'l Haifa Verification Conf. on Hardware and Software: Verification and Testing, volume 10629 of Lecture Notes in Computer Science, pages 147-162. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-70389-3_10.
  2. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. Symbolic LTLf synthesis. In Proc. 26th Int'l Joint Conf. on Artificial Intelligence, pages 1362-1369. ijcai.org, 2017. URL: http://dx.doi.org/10.24963/ijcai.2017/189.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail