Showing 1–16 of 16 results for author: Gol, E A

Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba

Authors: İlker Işık, Ebru Aydin Gol, Ramazan Gokberk Cinbis

Abstract: Temporal logic is a framework for representing and reasoning about propositions that evolve over time. It is commonly used for specifying requirements in various domains, including hardware and software systems, as well as robotics. Specification mining or formula generation involves extracting temporal logic formulae from system traces and has numerous applications, such as detecting bugs and imp… ▽ More Temporal logic is a framework for representing and reasoning about propositions that evolve over time. It is commonly used for specifying requirements in various domains, including hardware and software systems, as well as robotics. Specification mining or formula generation involves extracting temporal logic formulae from system traces and has numerous applications, such as detecting bugs and improving interpretability. Although there has been a surge of deep learning-based methods for temporal logic satisfiability checking in recent years, the specification mining literature has been lagging behind in adopting deep learning methods despite their many advantages, such as scalability. In this paper, we introduce autoregressive models that can generate linear temporal logic formulae from traces, towards addressing the specification mining problem. We propose multiple architectures for this task: transformer encoder-decoder, decoder-only transformer, and Mamba, which is an emerging alternative to transformer models. Additionally, we devise a metric for quantifying the distinctiveness of the generated formulae and a straightforward algorithm to enforce the syntax constraints. Our experiments show that the proposed architectures yield promising results, generating correct and distinct formulae at a fraction of the compute cost needed for the combinatorial baseline. △ Less

Submitted 31 May, 2024; originally announced May 2024.

Comments: 20 pages, 15 figures

Optimal Policy Synthesis from A Sequence of Goal Sets with An Application to Electric Distribution System Restoration

Authors: İlker Işık, Onur Yigit Arpali, Ebru Aydin Gol

Abstract: Motivated by the post-disaster distribution system restoration problem, in this paper, we study the problem of synthesizing the optimal policy for a Markov Decision Process (MDP) from a sequence of goal sets. For each goal set, our aim is to both maximize the probability to reach and minimize the expected time to reach the goal set. The order of the goal sets represents their priority. In particul… ▽ More Motivated by the post-disaster distribution system restoration problem, in this paper, we study the problem of synthesizing the optimal policy for a Markov Decision Process (MDP) from a sequence of goal sets. For each goal set, our aim is to both maximize the probability to reach and minimize the expected time to reach the goal set. The order of the goal sets represents their priority. In particular, our aim is to generate a policy that is optimal with respect to the first goal set, and it is optimal with respect to the second goal set among the policies that are optimal with respect to the first goal set and so on. To synthesize such a policy, we iteratively filter the applicable actions according to the goal sets. We illustrate the developed method over sample distribution systems and disaster scenarios. △ Less

Submitted 5 April, 2024; originally announced April 2024.

Comments: 7th ADHS 2021 Conference Paper

Journal ref: IFAC-PapersOnLine Volume 54, Issue 5, 2021, Pages 271-276

Field Teams Coordination for Earthquake-Damaged Distribution System Energization

Authors: İlker Işık, Ebru Aydin Gol

Abstract: The re-energization of electrical distribution systems in a post-disaster scenario is of grave importance as most modern infrastructure systems rely heavily on the presence of electricity. This paper introduces a method to coordinate the field teams for the optimal energization of an electrical distribution system after an earthquake-induced blackout. The proposed method utilizes a Markov Decision… ▽ More The re-energization of electrical distribution systems in a post-disaster scenario is of grave importance as most modern infrastructure systems rely heavily on the presence of electricity. This paper introduces a method to coordinate the field teams for the optimal energization of an electrical distribution system after an earthquake-induced blackout. The proposed method utilizes a Markov Decision Process (MDP) to create an optimal energization strategy, which aims to minimize the expected time to energize each distribution system component. The travel duration of each team and the possible outcomes of the energization attempts are considered in the state transitions. The failure probabilities of the system components are computed using the fragility curves of structures and the Peak Ground Acceleration (PGA) values which are encoded to the MDP model via transition probabilities. Furthermore, the proposed solution offers several methods to determine the non-optimal actions during the construction of the MDP and eliminate them in order to improve the run-time performance without sacrificing the optimality of the solution. △ Less

Submitted 5 April, 2024; originally announced April 2024.

Comments: Accepted manuscript, published in Reliability Engineering & System Safety

Journal ref: Reliability Engineering & System Safety Volume 245, May 2024, 110050

Numerical determination of iron dust laminar flame speeds with the counterflow twin-flame technique

Authors: C. E. A. G. van Gool, T. Hazenberg, J. A. van Oijen, L. P. H. de Goey

Abstract: Iron dust counter-flow flames have been studied with the low-Mach-number combustion approximation. The model considers full coupling between the two phases, including particle/droplet drag. The dispersed phase flow strain relations are derived under the assumption of low Reynolds number conditions. The importance of solving a particle flow strain model is demonstrated by comparing three different… ▽ More Iron dust counter-flow flames have been studied with the low-Mach-number combustion approximation. The model considers full coupling between the two phases, including particle/droplet drag. The dispersed phase flow strain relations are derived under the assumption of low Reynolds number conditions. The importance of solving a particle flow strain model is demonstrated by comparing three different models: a free unstrained flame, a counter-flow flame where particle flow strain is assumed equal to gas flow strain and one case in which the particle flow strain is solved. All three cases showed preferential diffusion effects, due to the lack of diffusion of iron in the fuel mixture, e.g. DFe,m = 0. The preferential diffusion effect causes a peak in the fuel equivalence ratio in the preheat zone. At the burned side, the combined effect of strain and preferential diffusion showed a decrease in fuel equivalence ratio. Inertia effects, which are only included in the resolved particle flow strain case, counteract this effect and result in an increase of the fuel equivalence ratio at the burned side. A laminar flame speed analysis is performed and a recommendation is given on how to experimentally determine the flame speed in a counter-flow set-up. △ Less

Submitted 8 December, 2023; originally announced December 2023.

Comments: 20 pages, 11 figures

Timed Automata Robustness Analysis via Model Checking

Authors: Jaroslav Bendík, Ahmet Sencan, Ebru Aydin Gol, Ivana Černá

Abstract: 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, th… ▽ More 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. △ Less

Submitted 28 July, 2022; v1 submitted 18 August, 2021; originally announced August 2021.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 3 (July 29, 2022) lmcs:8375

Control Synthesis for Parametric Timed Automata under Unavoidability Specifications

Authors: Ebru Aydin Gol

Abstract: Timed automata (TA) is used for modeling systems with timing aspects. A TA extends a finite automaton with a set of real valued variables called clocks, that measure the time and constraints over the clocks guard the transitions. A parametric TA (PTA) is a TA extension that allows parameters in clock constraints. In this paper, we focus on synthesis of a control strategy and parameter valuation fo… ▽ More Timed automata (TA) is used for modeling systems with timing aspects. A TA extends a finite automaton with a set of real valued variables called clocks, that measure the time and constraints over the clocks guard the transitions. A parametric TA (PTA) is a TA extension that allows parameters in clock constraints. In this paper, we focus on synthesis of a control strategy and parameter valuation for a PTA such that each run of the resulting TA reaches a target location within the given amount of time while avoiding unsafe locations. We propose an algorithm based on depth first analysis combined with an iterative feasibility check. The algorithm iteratively constructs a symbolic representation of the possible solutions, and employs a feasibility check to terminate the exploration along infeasible directions. Once the construction is completed, a mixed integer linear program is solved for each candidate strategy to generate a parameter valuation and a control strategy pair. We present a robotic planning example to motivate the problem and to illustrate the results. △ Less

Submitted 19 April, 2021; originally announced April 2021.

Comments: Submitted to ECC'21

Kontrol Edilebilir ptSTL Formulu Sentezi -- Synthesis of Controllable ptSTL Formulas

Authors: Irmak Saglam, Ebru Aydin Gol

Abstract: In this work, we develop an approach to anomaly detection and prevention problem using Signal Temporal Logic (STL). This approach consists of two steps: detection of the causes of the anomalities as STL formulas and prevention of the satisfaction of the formula via controller synthesis. This work focuses on the first step and proposes a formula template such that any controllable cause can be repr… ▽ More In this work, we develop an approach to anomaly detection and prevention problem using Signal Temporal Logic (STL). This approach consists of two steps: detection of the causes of the anomalities as STL formulas and prevention of the satisfaction of the formula via controller synthesis. This work focuses on the first step and proposes a formula template such that any controllable cause can be represented in this template. An efficient algorithm to synthesize formulas in this template is presented. Finally, the results are shown on an example. ----- Bu bildiride anomali tespiti ve onlenmesi problemine, Sinyal Zamansal Mantigi (Signal Temporal Logic) tabanli iki asamali bir cozum sunulmaktadir. Ilk asama nedenlerin tespiti, ikinci asama ise bir kontrol stratejisi ile nedenlerin sistem uzerinde engellenmesidir. Iki asama birbirine bagimlidir. Bu bildiride, ilk asama olan istenmeyen olaylarin nedenlerinin tespitinde kullanilan neden formulu sablonu gelistirilmektedir. Bildiride kullanilan sablon ile butun kontrol edilebilir formuller tanimlanabilmektedir. Bu sablon icin verimli bir formul sentezleme algoritmasi sunulmus, ve sonuclar ornek bir sistem uzerinde gosterilmistir. △ Less

Submitted 22 March, 2020; originally announced March 2020.

Comments: in Turkish

MSC Class: 03B70 ACM Class: F.4.1; F.4.3; I.2.4

A Novel MDP Based Decision Support Framework to Restore Earthquake Damaged Distribution Systems

Authors: Ebru Aydin Gol, Burcu Güldür Erkal, Murat Göl

Abstract: Electric power network expanded rapidly in recent decades due of the excessive need of electricity in every aspect of life, including critical infrastructures such as medical services, and transportation and communication systems. Natural disasters are one of the major reasons of electricity outage. It is extremely important to restore electrical energy in the shortest time possible after a disast… ▽ More Electric power network expanded rapidly in recent decades due of the excessive need of electricity in every aspect of life, including critical infrastructures such as medical services, and transportation and communication systems. Natural disasters are one of the major reasons of electricity outage. It is extremely important to restore electrical energy in the shortest time possible after a disaster. This paper proposes a decision support method for electric system operators to restore electricity to the critical loads in a distribution system after an earthquake. The proposed method employs Markov Decision Process to find the optimal restoration scheme based on the Probability of Failure of critical structures determined by using the Peak Ground Acceleration values recorded by observatories and earthquake research centers during earthquakes. △ Less

Submitted 13 November, 2019; originally announced November 2019.

Comments: Presented in ISGT 2019

MDP based Decision Support for Earthquake Damaged Distribution System Restoration

Authors: Onur Yigit Arpali, Ugur Can Yilmaz, Ebru Aydin Gol, Burcu Guldur Erkal, Murat Gol

Abstract: As the society becomes more dependent on the presence of electricity, the resilience of the power systems gains more importance. This paper develops a decision support method for distribution system operators to restore electricity after an earthquake to the maximum number of customers in the minimum expected duration. The proposed method employs Markov Decision Process (MDP) to determine the opti… ▽ More As the society becomes more dependent on the presence of electricity, the resilience of the power systems gains more importance. This paper develops a decision support method for distribution system operators to restore electricity after an earthquake to the maximum number of customers in the minimum expected duration. The proposed method employs Markov Decision Process (MDP) to determine the optimal restoration scheme. In order to determine the probability of the field component damage due to the earthquake, the Probability of Failure ($P_f$) of structures are calculated using the Peak Ground Acceleration (PGA) values recorded by observatories and earthquake research centers during the earthquake. △ Less

Submitted 11 November, 2019; v1 submitted 8 November, 2019; originally announced November 2019.

ATAC: A Tool for Automating Timed Automata Construction

Authors: Beyazit Yalcinkaya, Ebru Aydin Gol

Abstract: In this paper, we focus on the design and verification of timed automata (TA). We introduce a new method for assisting construction and verification of TA models along with a tool implementing the proposed method, i.e., ATAC: Automated Timed Automata Construction. Our method provides two main functionalities, i.e., construction of TA models from descriptions and generation of temporal logic querie… ▽ More In this paper, we focus on the design and verification of timed automata (TA). We introduce a new method for assisting construction and verification of TA models along with a tool implementing the proposed method, i.e., ATAC: Automated Timed Automata Construction. Our method provides two main functionalities, i.e., construction of TA models from descriptions and generation of temporal logic queries from specifications. Both description and specification sentences shall follow our well-defined structured natural language definition. TA models constructed from descriptions and temporal logic queries generated from specifications can be imported to UPPAAL, a verification tool for TA models. The goal is to accelerate the design phase for real-time systems by assisting the construction and verification of a formal model. We believe ATAC can be useful especially during the initial phases of the design process and help designers to avoid erroneous models. △ Less

Submitted 1 July, 2020; v1 submitted 20 May, 2019; originally announced May 2019.

Comments: 10 pages, 1 figure, tool paper

An Efficient Formula Synthesis Method with Past Signal Temporal Logic

Authors: Mert Ergurtuna, Ebru Aydin Gol

Abstract: In this work, we propose a novel method to find temporal properties that lead to the unexpected behaviors from labeled dataset. We express these properties in past time Signal Temporal Logic (ptSTL). First, we present a novel approach for finding parameters of a template ptSTL formula, which extends the results on monotonicity based parameter synthesis. The proposed method optimizes a given monoto… ▽ More In this work, we propose a novel method to find temporal properties that lead to the unexpected behaviors from labeled dataset. We express these properties in past time Signal Temporal Logic (ptSTL). First, we present a novel approach for finding parameters of a template ptSTL formula, which extends the results on monotonicity based parameter synthesis. The proposed method optimizes a given monotone criteria while bounding an error. Then, we employ the parameter synthesis method in an iterative unguided formula synthesis framework. In particular, we combine optimized formulas iteratively to describe the causes of the labeled events while bounding the error. We illustrate the proposed framework on two examples. △ Less

Submitted 16 April, 2019; originally announced April 2019.

Comments: 8 pages, 5 figures, conference paper

Cause Mining and Controller Synthesis with STL

Authors: Irmak Saglam, Ebru Aydin Gol

Abstract: Formal control of cyber-physical systems allows for synthesis of control strategies from rich specifications such as temporal logics. However, the classes of systems that the formal approaches can be applied to is limited due to the computational complexity. Furthermore, the synthesis problem becomes even harder when non-determinism or stochasticity is considered. In this work, we propose an alter… ▽ More Formal control of cyber-physical systems allows for synthesis of control strategies from rich specifications such as temporal logics. However, the classes of systems that the formal approaches can be applied to is limited due to the computational complexity. Furthermore, the synthesis problem becomes even harder when non-determinism or stochasticity is considered. In this work, we propose an alternative approach. First, we mark the unwanted events on the traces of the system and generate a controllable cause representing these events as a Signal Temporal Logic (STL) formula. Then, we synthesize a controller based on this formula to avoid the satisfaction of it. Our approach is applicable to any system with finitely many control choices. While we can not guarantee correctness, i.e., the unwanted events will never occur, we show on an example that the proposed approach reduces the number of the unwanted events. In particular, we validate it for the congestion avoidance problem in a traffic network. △ Less

Submitted 3 September, 2019; v1 submitted 7 April, 2019; originally announced April 2019.

A Formal Methods Approach to Pattern Synthesis in Reaction Diffusion Systems

Authors: Ebru Aydin Gol, Ezio Bartocci, Calin Belta

Abstract: We propose a technique to detect and generate patterns in a network of locally interacting dynamical systems. Central to our approach is a novel spatial superposition logic, whose semantics is defined over the quad-tree of a partitioned image. We show that formulas in this logic can be efficiently learned from positive and negative examples of several types of patterns. We also demonstrate that pa… ▽ More We propose a technique to detect and generate patterns in a network of locally interacting dynamical systems. Central to our approach is a novel spatial superposition logic, whose semantics is defined over the quad-tree of a partitioned image. We show that formulas in this logic can be efficiently learned from positive and negative examples of several types of patterns. We also demonstrate that pattern detection, which is implemented as a model checking algorithm, performs very well for test data sets different from the learning sets. We define a quantitative semantics for the logic and integrate the model checking algorithm with particle swarm optimization in a computational framework for synthesis of parameters leading to desired patterns in reaction-diffusion systems. △ Less

Submitted 12 September, 2014; originally announced September 2014.

Traffic Network Control from Temporal Logic Specifications

Authors: Samuel Coogan, Ebru Aydin Gol, Murat Arcak, Calin Belta

Abstract: We propose a framework for generating a signal control policy for a traffic network of signalized intersections to accomplish control objectives expressible using linear temporal logic. By applying techniques from model checking and formal methods, we obtain a correct-by-construction controller that is guaranteed to satisfy complex specifications. To apply these tools, we identify and exploit stru… ▽ More We propose a framework for generating a signal control policy for a traffic network of signalized intersections to accomplish control objectives expressible using linear temporal logic. By applying techniques from model checking and formal methods, we obtain a correct-by-construction controller that is guaranteed to satisfy complex specifications. To apply these tools, we identify and exploit structural properties particular to traffic networks that allow for efficient computation of a finite state abstraction. In particular, traffic networks exhibit a componentwise monotonicity property which allows reach set computations that scale linearly with the dimension of the continuous state space. △ Less

Submitted 21 June, 2016; v1 submitted 6 August, 2014; originally announced August 2014.

Journal ref: IEEE Transactions on Control of Network Systems, vol. 3, no. 2, pp. 162-172, June 2016

Finite Bisimulations for Switched Linear Systems

Authors: Ebru Aydin Gol, Xuchu Ding, Mircea Lazar, Calin Belta

Abstract: In this paper, we consider the problem of constructing a finite bisimulation quotient for a discrete-time switched linear system in a bounded subset of its state space. Given a set of observations over polytopic subsets of the state space and a switched linear system with stable subsystems, the proposed algorithm generates the bisimulation quotient in a finite number of steps with the aid of suble… ▽ More In this paper, we consider the problem of constructing a finite bisimulation quotient for a discrete-time switched linear system in a bounded subset of its state space. Given a set of observations over polytopic subsets of the state space and a switched linear system with stable subsystems, the proposed algorithm generates the bisimulation quotient in a finite number of steps with the aid of sublevel sets of a polyhedral Lyapunov function. Starting from a sublevel set that includes the origin in its interior, the proposed algorithm iteratively constructs the bisimulation quotient for any larger sublevel set. The bisimulation quotient can then be further used for synthesis of the switching law and system verification with respect to specifications given as syntactically co-safe Linear Temporal Logic formulas over the observed polytopic subsets. △ Less

Submitted 27 August, 2012; originally announced August 2012.

Time-Constrained Temporal Logic Control of Multi-Affine Systems

Authors: Ebru Aydin Gol, Calin Belta

Abstract: In this paper, we consider the problem of controlling a dynamical system such that its trajectories satisfy a temporal logic property in a given amount of time. We focus on multi-affine systems and specifications given as syntactically co-safe linear temporal logic formulas over rectangular regions in the state space. The proposed algorithm is based on the estimation of time bounds for facet reach… ▽ More In this paper, we consider the problem of controlling a dynamical system such that its trajectories satisfy a temporal logic property in a given amount of time. We focus on multi-affine systems and specifications given as syntactically co-safe linear temporal logic formulas over rectangular regions in the state space. The proposed algorithm is based on the estimation of time bounds for facet reachability problems and solving a time optimal reachability problem on the product between a weighted transition system and an automaton that enforces the satisfaction of the specification. A random optimization algorithm is used to iteratively improve the solution. △ Less

Submitted 26 March, 2012; originally announced March 2012.

ACM Class: I.2.8; D.2.4