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 language | English (US) |
|---|---|
| Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 294-309 |
| Number of pages | 16 |
| Volume | 7186 LNCS |
| DOIs | |
| State | Published - 2012 |
| Event | 2nd International Conference on Runtime Verification, RV 2011 - San Francisco, CA, United States Duration: Sep 27 2011 → Sep 30 2011 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 7186 LNCS |
| ISSN (Print) | 03029743 |
| ISSN (Electronic) | 16113349 |
Other
| Other | 2nd International Conference on Runtime Verification, RV 2011 |
|---|---|
| Country | United States |
| City | San Francisco, CA |
| Period | 9/27/11 → 9/30/11 |
Fingerprint
ASJC Scopus subject areas
- Computer Science(all)
- Theoretical Computer Science
Cite this
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 proceeding › Conference contribution
}
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 -