Combining time and frequency domain specifications for periodic signals

Aleksandar Chakarov, Sriram Sankaranarayanan, Georgios Fainekos

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

In this paper, we investigate formalisms for specifying periodic signals using time and frequency domain specifications along with algorithms for the signal recognition and generation problems for such specifications. The time domain specifications are in the form of hybrid automata whose continuous state variables generate the desired signals. The frequency domain specifications take the form of an "envelope" that constrains the possible power spectra of the periodic signals with a given frequency cutoff. The combination of time and frequency domain specifications yields mixed-domain specifications that constrain a signal to belong to the intersection of the both specifications. We show that the signal recognition problem for periodic signals specified by hybrid automata is NP-complete, while the corresponding problem for frequency domain specifications can be approximated to any desired degree by linear programs, which can be solved in polynomial time. The signal generation problem for time and frequency domain specifications can be encoded into linear arithmetic constraints that can be solved using existing SMT solvers. We present some preliminary results based on an implementation that uses the SMT solver Z3 to tackle the signal generation problems.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages294-309
Number of pages16
Volume7186 LNCS
DOIs
StatePublished - 2012
Event2nd International Conference on Runtime Verification, RV 2011 - San Francisco, CA, United States
Duration: Sep 27 2011Sep 30 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7186 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other2nd International Conference on Runtime Verification, RV 2011
CountryUnited States
CitySan Francisco, CA
Period9/27/119/30/11

Fingerprint

Frequency Domain
Time Domain
Specification
Specifications
Hybrid Automata
Surface mount technology
Cutoff frequency
Power spectrum
Power Spectrum
Linear Program
Envelope
Polynomial time
NP-complete problem
Intersection
Polynomials

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Chakarov, A., Sankaranarayanan, S., & Fainekos, G. (2012). Combining time and frequency domain specifications for periodic signals. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7186 LNCS, pp. 294-309). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7186 LNCS). https://doi.org/10.1007/978-3-642-29860-8_22

Combining time and frequency domain specifications for periodic signals. / Chakarov, Aleksandar; Sankaranarayanan, Sriram; Fainekos, Georgios.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7186 LNCS 2012. p. 294-309 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7186 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Chakarov, A, Sankaranarayanan, S & Fainekos, G 2012, Combining time and frequency domain specifications for periodic signals. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 7186 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7186 LNCS, pp. 294-309, 2nd International Conference on Runtime Verification, RV 2011, San Francisco, CA, United States, 9/27/11. https://doi.org/10.1007/978-3-642-29860-8_22
Chakarov A, Sankaranarayanan S, Fainekos G. Combining time and frequency domain specifications for periodic signals. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7186 LNCS. 2012. p. 294-309. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-29860-8_22
Chakarov, Aleksandar ; Sankaranarayanan, Sriram ; Fainekos, Georgios. / Combining time and frequency domain specifications for periodic signals. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7186 LNCS 2012. pp. 294-309 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c0c73c7fe72b4808b9351340fd194b16,
title = "Combining time and frequency domain specifications for periodic signals",
abstract = "In this paper, we investigate formalisms for specifying periodic signals using time and frequency domain specifications along with algorithms for the signal recognition and generation problems for such specifications. The time domain specifications are in the form of hybrid automata whose continuous state variables generate the desired signals. The frequency domain specifications take the form of an {"}envelope{"} that constrains the possible power spectra of the periodic signals with a given frequency cutoff. The combination of time and frequency domain specifications yields mixed-domain specifications that constrain a signal to belong to the intersection of the both specifications. We show that the signal recognition problem for periodic signals specified by hybrid automata is NP-complete, while the corresponding problem for frequency domain specifications can be approximated to any desired degree by linear programs, which can be solved in polynomial time. The signal generation problem for time and frequency domain specifications can be encoded into linear arithmetic constraints that can be solved using existing SMT solvers. We present some preliminary results based on an implementation that uses the SMT solver Z3 to tackle the signal generation problems.",
author = "Aleksandar Chakarov and Sriram Sankaranarayanan and Georgios Fainekos",
year = "2012",
doi = "10.1007/978-3-642-29860-8_22",
language = "English (US)",
isbn = "9783642298592",
volume = "7186 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "294--309",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Combining time and frequency domain specifications for periodic signals

AU - Chakarov, Aleksandar

AU - Sankaranarayanan, Sriram

AU - Fainekos, Georgios

PY - 2012

Y1 - 2012

N2 - In this paper, we investigate formalisms for specifying periodic signals using time and frequency domain specifications along with algorithms for the signal recognition and generation problems for such specifications. The time domain specifications are in the form of hybrid automata whose continuous state variables generate the desired signals. The frequency domain specifications take the form of an "envelope" that constrains the possible power spectra of the periodic signals with a given frequency cutoff. The combination of time and frequency domain specifications yields mixed-domain specifications that constrain a signal to belong to the intersection of the both specifications. We show that the signal recognition problem for periodic signals specified by hybrid automata is NP-complete, while the corresponding problem for frequency domain specifications can be approximated to any desired degree by linear programs, which can be solved in polynomial time. The signal generation problem for time and frequency domain specifications can be encoded into linear arithmetic constraints that can be solved using existing SMT solvers. We present some preliminary results based on an implementation that uses the SMT solver Z3 to tackle the signal generation problems.

AB - In this paper, we investigate formalisms for specifying periodic signals using time and frequency domain specifications along with algorithms for the signal recognition and generation problems for such specifications. The time domain specifications are in the form of hybrid automata whose continuous state variables generate the desired signals. The frequency domain specifications take the form of an "envelope" that constrains the possible power spectra of the periodic signals with a given frequency cutoff. The combination of time and frequency domain specifications yields mixed-domain specifications that constrain a signal to belong to the intersection of the both specifications. We show that the signal recognition problem for periodic signals specified by hybrid automata is NP-complete, while the corresponding problem for frequency domain specifications can be approximated to any desired degree by linear programs, which can be solved in polynomial time. The signal generation problem for time and frequency domain specifications can be encoded into linear arithmetic constraints that can be solved using existing SMT solvers. We present some preliminary results based on an implementation that uses the SMT solver Z3 to tackle the signal generation problems.

UR - http://www.scopus.com/inward/record.url?scp=84861208330&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84861208330&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-29860-8_22

DO - 10.1007/978-3-642-29860-8_22

M3 - Conference contribution

SN - 9783642298592

VL - 7186 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 294

EP - 309

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -