dissertation · Arizona State University Library Digital Repository (Arizona State University) · 2013

Dynamic Programming algorithm for Computing Temporal Logic Robustness

R Alur, T Henzinger, G Fainekos, G Pappas, Ron Koymans, A Seda, P Hitzler, G Rou, K Havelund, Oded Maler, Amir Pnueli, R Baber, A Donze, O Maler, E Asarin, A Donz, O Maler, D Nickovic, Hengyi Yang, Bardh Hoxha, E Georgios, H Abbas, G Fainekos, S Sankaranarayanan, F Ivancic, A Gupta, Q Zhao, B Krogh, P Hubbard, A Cimatti, M Roveri, D Sheridan, Georgios Fainekos, Koichi Sriram Sankaranarayanan, Hakan Ueda, Yazarel, Sriram Sankaranarayanan, Georgios Fainekos, A Donze, Georgios Fainekos, George Pappas, Georgios Fainekos, George Pappas, Georgios Fainekos, George Pappas, Y Annapureddy, C Liu, G Fainekos, S Sankaranarayanan, S-Taliro and 34 more

Cited by 0Open access

Abstract

abstract: In this thesis we deal with the problem of temporal logic robustness estimation. We present a dynamic programming algorithm for the robust estimation problem of Metric Temporal Logic (MTL) formulas regarding a finite trace of time stated sequence. This algorithm not only tests if the MTL specification is satisfied by the given input which is a finite system trajectory, but also quantifies to what extend does the sequence satisfies or violates the MTL specification. The implementation of the algorithm is the DP-TALIRO toolbox for MATLAB. Currently it is used as the temporal logic robust computing engine of S-TALIRO which is a tool for MATLAB searching for trajectories of minimal robustness in Simulink/ Stateflow. DP-TALIRO is expected to have near linear running time and constant memory requirement depending on the structure of the MTL formula. DP-TALIRO toolbox also integrates new features not supported in its ancestor FW-TALIRO such as parameter replacement, most related iteration and most related predicate. A derivative of DP-TALIRO which is DP-T-TALIRO is also addressed in this thesis which applies dynamic programming algorithm for time robustness computation. We test the running time of DP-TALIRO and compare it with FW-TALIRO. Finally, we present an application where DP-TALIRO is used as the robustness computation core of S-TALIRO for a parameter estimation problem.

Cite this paper

APA 7

Alur, R., Henzinger, T., Fainekos, G., Pappas, G., Koymans, R., Seda, A., Hitzler, P., Rou, G., Havelund, K., Maler, O., Pnueli, A., Baber, R., Donze, A., Maler, O., Asarin, E., Donz, A., Maler, O., Nickovic, D., Yang, H., . . . S-Taliro. (2013). Dynamic Programming algorithm for Computing Temporal Logic Robustness. Arizona State University Library Digital Repository (Arizona State University).

MLA 9

Alur, R, et al. “Dynamic Programming algorithm for Computing Temporal Logic Robustness.” Arizona State University Library Digital Repository (Arizona State University), 2013.

Chicago

Alur, R, T Henzinger, G Fainekos, G Pappas, Ron Koymans, A Seda, P Hitzler, et al. 2013. “Dynamic Programming algorithm for Computing Temporal Logic Robustness.” Arizona State University Library Digital Repository (Arizona State University).

Harvard

Alur, R. et al. (2013) ‘Dynamic Programming algorithm for Computing Temporal Logic Robustness’, Arizona State University Library Digital Repository (Arizona State University).

BibTeX

@phdthesis{alur2013dynamic,
  title = {{Dynamic Programming algorithm for Computing Temporal Logic Robustness}},
  author = {Alur, R and Henzinger, T and Fainekos, G and Pappas, G and Koymans, Ron and Seda, A and Hitzler, P and Rou, G and Havelund, K and Maler, Oded and Pnueli, Amir and Baber, R and Donze, A and Maler, O and Asarin, E and Donz, A and Maler, O and Nickovic, D and Yang, Hengyi and Hoxha, Bardh and Georgios, E and Abbas, H and Fainekos, G and Sankaranarayanan, S and Ivancic, F and Gupta, A and Zhao, Q and Krogh, B and Hubbard, P and Cimatti, A and Roveri, M and Sheridan, D and Fainekos, Georgios and Sankaranarayanan, Koichi Sriram and Ueda, Hakan and Yazarel and Sankaranarayanan, Sriram and Fainekos, Georgios and Donze, A and Fainekos, Georgios and Pappas, George and Fainekos, Georgios and Pappas, George and Fainekos, Georgios and Pappas, George and Annapureddy, Y and Liu, C and Fainekos, G and Sankaranarayanan, S and S-Taliro and others},
  school = {Arizona State University Library Digital Repository (Arizona State University)},
  year = {2013}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.