scholarly journals Parameterised Resource-Bounded ATL

2020 ◽  
Vol 34 (05) ◽  
pp. 7040-7046
Author(s):  
Natasha Alechina ◽  
Stéphane Demri ◽  
Brian Logan
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Parameter Extraction ◽  
Resource Requirement ◽  
Extraction Algorithm ◽  
Resource Requirements ◽  
Strategic Ability ◽  
Resource Logics

It is often advantageous to be able to extract resource requirements in resource logics of strategic ability, rather than to verify whether a fixed resource requirement is sufficient for achieving a goal. We study Parameterised Resource-Bounded Alternating Time Temporal Logic where parameter extraction is possible. We give a parameter extraction algorithm and prove that the model-checking problem is 2EXPTIME-complete.

scholarly journals Timed ATL: Forget Memory, Just Count

2019 ◽  
Vol 66 ◽  
pp. 197-223
Author(s):  
Michal Jozef Knapik ◽  
Etienne Andre ◽  
Laure Petrucci ◽  
Wojciech Jamroga ◽  
Wojciech Penczek
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Discrete Time ◽  
The Other ◽  
Simple Pattern ◽  
Perfect Recall ◽  
Other Hand ◽  
Compact Representations ◽  
Time Extension ◽  
Number Of Visits

In this paper we investigate the Timed Alternating-Time Temporal Logic (TATL), a discrete-time extension of ATL. In particular, we propose, systematize, and further study semantic variants of TATL, based on different notions of a strategy. The notions are derived from different assumptions about the agents’ memory and observational capabilities, and range from timed perfect recall to untimed memoryless plans. We also introduce a new semantics based on counting the number of visits to locations during the play. We show that all the semantics, except for the untimed memoryless one, are equivalent when punctuality constraints are not allowed in the formulae. In fact, abilities in all those notions of a strategy collapse to the “counting” semantics with only two actions allowed per location. On the other hand, this simple pattern does not extend to the full TATL. As a consequence, we establish a hierarchy of TATL semantics, based on the expressivity of the underlying strategies, and we show when some of the semantics coincide. In particular, we prove that more compact representations are possible for a reasonable subset of TATL specifications, which should improve the efficiency of model checking and strategy synthesis.

An Analytical Model for Resource Characterization and Parameter Estimation for DAG-Based Jobs for Homogeneous Systems

2015 ◽  
Vol 6 (1) ◽  
pp. 34-52 ◽  
Author(s):  
Mohammad Sajid ◽  
Zahid Raza
Keyword(s):  
Analytical Model ◽  
High Performance ◽  
Service Providers ◽  
Average Energy ◽  
Electrical Energy ◽  
Turnaround Time ◽  
Service Level ◽  
Resource Requirement ◽  
Service Oriented Architectures ◽  
Resource Requirements

High Performance Computing (HPC) systems demand and consume a significant amount of resources (e.g. server, storage, electrical energy) resulting in high operational costs, reduced reliability, and sometimes leading to waste of scarce natural resources. On one hand, the most important issue for these systems is achieving high performance, while on the other hand, the rapidly increasing resource costs appeal to effectively predict the resource requirements to ensure efficient services in the most optimized manner. The resource requirement prediction for a job thus becomes important for both the service providers as well as the consumers for ensuring resource management and to negotiate Service Level Agreements (SLAs), respectively, in order to help make better job allocation decisions. Moreover, the resource requirement prediction can even lead to improved scheduling performance while reducing the resource waste. This work presents an analytical model estimating the required resources for the modular job execution. The analysis identifies the number of processors required and the maximum and minimum bounds on the turnaround time and energy consumed. Simulation study reveals that the scheduling algorithms integrated with the proposed analytical model helps in improving the average throughput and the average energy consumption of the system. As the work predicts the resource requirements, it can even play an important role in Service-Oriented Architectures (SOA) like Cloud computing or Grid computing.

scholarly journals Model Checking Temporal Logic Formulas Using Sticker Automata

2017 ◽  
Vol 2017 ◽  
pp. 1-33 ◽  
Author(s):  
Weijun Zhu ◽  
Changwei Feng ◽  
Huanmei Wu
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Complex Problem ◽  
Finite State Automaton ◽  
Dna Molecules ◽  
Single Stranded Dna ◽  
Finite State ◽  
Input Strings ◽  
Logic Model Checking ◽  
The Given

As an important complex problem, the temporal logic model checking problem is still far from being fully resolved under the circumstance of DNA computing, especially Computation Tree Logic (CTL), Interval Temporal Logic (ITL), and Projection Temporal Logic (PTL), because there is still a lack of approaches for DNA model checking. To address this challenge, a model checking method is proposed for checking the basic formulas in the above three temporal logic types with DNA molecules. First, one-type single-stranded DNA molecules are employed to encode the Finite State Automaton (FSA) model of the given basic formula so that a sticker automaton is obtained. On the other hand, other single-stranded DNA molecules are employed to encode the given system model so that the input strings of the sticker automaton are obtained. Next, a series of biochemical reactions are conducted between the above two types of single-stranded DNA molecules. It can then be decided whether the system satisfies the formula or not. As a result, we have developed a DNA-based approach for checking all the basic formulas of CTL, ITL, and PTL. The simulated results demonstrate the effectiveness of the new method.

scholarly journals ∞-Regular temporal logic and its model checking problem

1992 ◽  
Vol 103 (2) ◽  
pp. 191-204 ◽  
Author(s):  
Kiyoharu Hamaguchi ◽  
Hiromi Hiraishi ◽  
Shuzo Yajima
Keyword(s):  
Model Checking ◽  
Temporal Logic
Sign in / Sign up

Export Citation Format

Share Document