Clock Reduction in Timed Automata While Preserving Design Parameters

Date

2019-08-22

Author

Yancinkaya, Beyazit
Aydın Göl, Ebru

Metadata

Show full item record

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

Item Usage Stats

142
views

0
downloads

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 and transitions of the automaton reflect the modeled system's physical properties and design parameters; the proposed method changes the clock constraints based on their positions to reduce the total number of clocks. To guarantee correctness, we prove that the resulting automaton is timed bisimilar to the original one. Finally, we present empirical results for the solution, which show that the proposed method significantly reduces the clock count without changing design parameters of the system.

URI

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

DOI

https://doi.org/10.1109/formalise.2019.00010

Collections

Department of Computer Engineering, Conference / Seminar

Suggestions

OpenMETU
Core

TIMED AUTOMATA ROBUSTNESS ANALYSIS VIA MODEL CHECKING Bendik, Jaroslav; Sencan, Ahmet; Aydın Göl, Ebru; Cerna, Ivana (2022-01-01) 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 t...
Causal and Passive Parameterization of S-Parameters Using Neural Networks Torun, Hakki Mert; Durgun, Ahmet Cemal; Aygun, Kemal; Swaminathan, Madhavan (Institute of Electrical and Electronics Engineers (IEEE), 2020-10-01) Neural networks (NNs) are widely used to create parametric models of S-parameters for various components in electronic systems. The focus of deriving these models has so far been numerical error reduction between the NN-generated S-parameters and the data source. However, this is not sufficient when creating such NNs since it does not guarantee predicted S-parameters to be physically consistent, i.e., passive and causal, which restricts their use cases. This article, therefore, proposes a causality enforcem...
Stochastic modelling of biochemical networks and inference of modelparameters Purutçuoğlu Gazi, Vilda (null, Springer, 2018-01-01) There are many approaches to model the biochemical systems deterministically or stochastically. In deterministic approaches, we aim to describe the steady-state behaviours of the system, whereas, under stochastic models, we present the random nature of the system, for instance, during transcription or translation processes. Here, we represent the stochastic modelling approaches of biological networks and explain in details the inference of the model parameters within the Bayesian framework.
Power-delay optimized VLSI threshold detection circuits and their use in parallel integer multiplication Ercan, Furkan; Muhtaroğlu, Ali; Sustainable Environment and Energy Systems (2015-6) Threshold detection is a fundamental logic function that has broad use in arithmetic processors, and other digital applications. Thus, any improvement in threshold detection in terms of power and/or delay contributes significantly to the field of digital circuit design. A recently reported parallel integer multiplier architecture, ABACUS, uses column compression networks to compress partial products through the final addition network. Architecture of column compression network of ABACUS is suitable for thre...
Direction finding performance of antenna arrays on complex platforms using numerical electromagnetic simulation tools Özeç, Mustafa Onur; Tuncer, Temel Engin; Department of Electrical and Electronics Engineering (2011) An important step for the design of direction finding systems is the performance evaluation using numeric electromagnetic simulation tools. In this thesis, a method is presented for both modeling and simulation in a numeric electromagnetic simulation tool FEKO. The method relies on the data generated by FEKO. The data is then processed by correlative interferometer algorithm. This process is implemented in a MATLAB environment. Different types of antenna arrays including dipole, monopole and discone antenna...

Citation Formats

B. Yancinkaya and E. Aydın Göl, “Clock Reduction in Timed Automata While Preserving Design Parameters,” 2019, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/35542.