BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Ebru Aydin Gol

Ebru Aydin Gol appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Systems and ControlFormal Languages and Automata TheoryLogic in Computer Sciencemath.DSArtificial IntelligenceComputational Engineering, Finance, and Scienceeess.SYMachine Learning

Catalog footprint

What is connected

6works
8topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

6 published item(s)

preprint2020arXiv

ATAC: A Tool for Automating Timed Automata Construction

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Traffic Network Control from Temporal Logic Specifications

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

A Formal Methods Approach to Pattern Synthesis in Reaction Diffusion Systems

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Finite Bisimulations for Switched Linear Systems

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Time-Constrained Temporal Logic Control of Multi-Affine Systems

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.

0 citations0 reviewsNo code linkedOpen access