TIMED AUTOMATA ROBUSTNESS ANALYSIS VIA MODEL CHECKING

Date

2022-01-01

Author

Bendik, Jaroslav
Sencan, Ahmet
Aydın Göl, Ebru
Cerna, Ivana

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

76
views

0
downloads

Timed automata (TA) have been widely adopted as a suitable formalism to model time-critical systems. Furthermore, contemporary model-checking tools allow the designer to check whether a TA complies with a system specification. However, the exact timing constants are often uncertain during the design phase. Consequently, the designer is often able to build a TA with a correct structure, however, the timing constants need to be tuned to satisfy the specification. Moreover, even if the TA initially satisfies the specification, it can be the case that just a slight perturbation during the implementation causes a violation of the specification. Unfortunately, model-checking tools are usually not able to provide any reasonable guidance on how to fix the model in such situations. In this paper, we propose several concepts and techniques to cope with the above mentioned design phase issues when dealing with reachability and safety specifications.

Subject Keywords

Timed Automata, Design, Reachability, Safety, LTL PARAMETER SYNTHESIS, VERIFICATION, SUBSETS

URI

https://hdl.handle.net/11511/98910

Journal

LOGICAL METHODS IN COMPUTER SCIENCE

DOI

https://doi.org/10.46298/lmcs-18(3:12)2022

Collections

Department of Computer Engineering, Article

Suggestions

OpenMETU
Core

Clock Reduction in Timed Automata While Preserving Design Parameters Yancinkaya, Beyazit; Aydın Göl, Ebru (2019-08-22) Timed automata (TA) are widely used to model and verify real-time systems. In a TA, the real valued variables, called clocks, measure the time passed between events. The verification of TA is exponential in the number of clocks. That constitutes a bottleneck for its application in large systems. To address this issue, we propose a novel clock reduction method. We aim at reducing the number of clocks by developing a position (location and transition) based mapping for clocks. Motivated by that the locations ...
Time series classification with feature covariance matrices Ergezer, Hamza; Leblebicioğlu, Mehmet Kemal (2018-06-01) In this work, a novel approach utilizing feature covariance matrices is proposed for time series classification. In order to adapt the feature covariance matrices into time series classification problem, a feature vector is defined for each point in a time series. The feature vector comprises local and global information such as value, derivative, rank, deviation from the mean, the time index of the point and cumulative sum up to the point. Extracted feature vectors for the time instances are concatenated t...
Blind Deinterleaving of Signals in Time Series with Self-Attention Based Soft Min-Cost Flow Learning Can, Oğul; Gürbüz, Yeti Ziya; Yildirim, Berkin; Alatan, Abdullah Aydın (2021-01-01) We propose an end-to-end learning approach to address deinterleaving of patterns in time series, in particular, radar signals. We link signal clustering problem to min-cost flow as an equivalent problem once the proper costs exist. We formulate a bi-level optimization problem involving min-cost flow as a sub-problem to learn such costs from the supervised training data. We then approximate the lower level optimization problem by self-attention based neural networks and provide a trainable framework that clu...
Multi-objective decision making using fuzzy discrete event systems: A mobile robot example Boutalis, Yiannis; Schmidt, Klaus Verner (2010-09-29) In this paper, we propose an approach for the multi-objective control of sampled data systems that can be modeled as fuzzy discrete event systems (FDES). In our work, the choice of a fuzzy system representation is justified by the assumption of a controller realization that depends on various potentially imprecise sensor measurements. Our approach consists of three basic steps that are performed in each sampling instant. First, the current fuzzy state of the system is determined by a sensor evaluation. Seco...
Loop-based conic multivariate adaptive regression splines is a novel method for advanced construction of complex biological networks Ayyıldız Demirci, Ezgi; Purutçuoğlu Gazi, Vilda; Weber, Gerhard Wilhelm (2018-11-01) The Gaussian Graphical Model (GGM) and its Bayesian alternative, called, the Gaussian copula graphical model (GCGM) are two widely used approaches to construct the undirected networks of biological systems. They define the interactions between species by using the conditional dependencies of the multivariate normality assumption. However, when the system's dimension is high, the performance of the model becomes computationally demanding, and, particularly, the accuracy of GGM decreases when the observations...

Citation Formats

J. Bendik, A. Sencan, E. Aydın Göl, and I. Cerna, “TIMED AUTOMATA ROBUSTNESS ANALYSIS VIA MODEL CHECKING,” LOGICAL METHODS IN COMPUTER SCIENCE, vol. 18, no. 3, pp. 0–0, 2022, Accessed: 00, 2022. [Online]. Available: https://hdl.handle.net/11511/98910.