Show/Hide Menu
Hide/Show Apps
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Open Science Policy
Open Science Policy
Open Access Guideline
Open Access Guideline
Postgraduate Thesis Guideline
Postgraduate Thesis Guideline
Communities & Collections
Communities & Collections
Help
Help
Frequently Asked Questions
Frequently Asked Questions
Guides
Guides
Thesis submission
Thesis submission
MS without thesis term project submission
MS without thesis term project submission
Publication submission with DOI
Publication submission with DOI
Publication submission
Publication submission
Supporting Information
Supporting Information
General Information
General Information
Copyright, Embargo and License
Copyright, Embargo and License
Contact us
Contact us
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
102
views
0
downloads
Cite This
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
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
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.