scholarly journals Minimum-Cost Reachability for Priced Timed Automata

2001 ◽  
Vol 8 (3) ◽  
Author(s):  
Gerd Behrmann ◽  
Ansgar Fehnker ◽  
Thomas S. Hune ◽  
Kim G. Larsen ◽  
Paul Pettersson ◽  
...  
Keyword(s):  
Branch And Bound ◽  
Data Structures ◽  
Timed Automata ◽  
Minimum Cost ◽  
Initial State ◽  
Reachability Problem ◽  
Algorithmic Solution ◽  
The Cost ◽  
Branch And Bound Techniques ◽  
Timed Automaton

<p>This paper introduces the model of linearly priced timed automata as an extension of timed automata, with prices on both transitions and locations. For this model we consider the minimum-cost reachability problem: i.e. given a linearly priced timed automaton and a target<br />state, determine the minimum cost of executions from the initial state to the target state. This problem generalizes the minimum-time reachability problem for ordinary timed automata. We prove decidability of this problem by offering an algorithmic solution, which is based on a combination of branch-and-bound techniques and a new notion of priced regions. The latter allows symbolic representation and manipulation of reachable states together with the cost of reaching them.</p><p>Keywords: Timed Automata, Verification, Data Structures, Algorithms,<br />Optimization.</p>

scholarly journals Model Checking via Reachability Testing for Timed Automata

1997 ◽  
Vol 4 (29) ◽  
Author(s):  
Luca Aceto ◽  
Augusto Burgueno ◽  
Kim G. Larsen
Keyword(s):  
Model Checking ◽  
Timed Automata ◽  
Reachability Problem ◽  
Liveness Properties ◽  
Time Logic ◽  
Definition Of ◽  
Reachability Testing ◽  
Time Systems ◽  
Timed Automaton ◽  
Theoretical Side

In this paper we develop an approach to model-checking for timed automata via reachability testing. As our specification formalism, we consider a dense-time logic with clocks. This logic may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every logical formula phi, a so-called test automaton T_phi in such a way that checking whether a system S satisfies the property phi can be reduced to a reachability question over the system obtained by making T_phi interact with S. <br />The testable logic we consider is both of practical and theoretical interest. On the practical side, we have used the logic, and the associated approach to model-checking via reachability testing it supports, in the specification and verification in Uppaal of a collision avoidance protocol. On the theoretical side, we show that the logic is powerful enough to permit the definition of characteristic properties, with respect to a timed version of<br />the ready simulation preorder, for nodes of deterministic, tau-free timed automata. This allows one to compute behavioural relations via our model-checking technique, therefore effectively reducing the problem of checking the existence of a behavioural relation among states of a timed automaton to a reachability problem.

FAST DETERMINISTIC PARALLEL BRANCH-AND-BOUND

1999 ◽  
Vol 09 (03) ◽  
pp. 325-333 ◽  
Author(s):  
KIERAN T. HERLEY ◽  
ANDREA PIETRACAPRINA ◽  
GEPPINO PUCCI
Keyword(s):  
Branch And Bound ◽  
Minimum Cost ◽  
Parallel Machine ◽  
Deterministic Algorithm ◽  
Local Computation ◽  
Running Time ◽  
Erew Pram ◽  
Constant Degree ◽  
Parallel Branch And Bound ◽  
The Cost

The branch-and-bound problem involves determining the minimum cost leaf in a cost-labelled tree, subject to the constraint that only the root is known initially and that children are revealed only by visiting thier parent. We present the first efficient deterministic algorithm to solve the branch-and-bound problem for a tree T of constant degree on a p-processor parallel machine. Let c* be the cost of the minimum-cost leaf in T, and let n and h be the number of nodes and the height, respectively, of the subtree T* ⊆ T of nodes of cost less than or equal to c*. Our algorithm runs in O(n/p + h log 2(np)) time on an EREW-PRAM. Moreover, the running time faithfully reflects both communication and computation costs, unlike most of the previous results where the cost of local computation is ignored. For large ranges of the parameters, our algorithm matches the optimal performance of existing randomized strategies. The algorithm can be ported to any architecture for which an efficient implementation of Parallel Priority Queues [PP91] is available.

scholarly journals Efficient Guiding Towards Cost-Optimality in UPPAAL

2001 ◽  
Vol 8 (4) ◽  
Author(s):  
Gerd Behrmann ◽  
Ansgar Fehnker ◽  
Thomas S. Hune ◽  
Kim G. Larsen ◽  
Paul Pettersson ◽  
...  
Keyword(s):  
Timed Automata ◽  
Minimum Cost ◽  
Search Space ◽  
Shortest Path Algorithm ◽  
Goal State ◽  
Verification Tool ◽  
Search Order ◽  
Efficient Representation ◽  
The Cost ◽  
Cost Optimality

<p>In this paper we present an algorithm for efficiently computing<br /> the minimum cost of reaching a goal state in the model of Uniformly<br />Priced Timed Automata (UPTA). This model can be seen as a submodel<br />of the recently suggested model of linearly priced timed automata, which<br />extends timed automata with prices on both locations and transitions.<br />The presented algorithm is based on a symbolic semantics of UTPA, and<br />an efficient representation and operations based on difference bound <br />matrices. In analogy with Dijkstra's shortest path algorithm, we show that<br />the search order of the algorithm can be chosen such that the number of<br />symbolic states explored by the algorithm is optimal, in the sense that<br />the number of explored states can not be reduced by any other search<br />order based on the cost of states. We also present a number of techniques<br />inspired by branch-and-bound algorithms which can be used for limiting<br />the search space and for quickly finding near-optimal solutions.<br />The algorithm has been implemented in the verification tool Uppaal.<br />When applied on a number of experiments the presented techniques <br />reduced the explored state-space with up to 90%.</p>

DETERMINISTIC BRANCH-AND-BOUND ON DISTRIBUTED MEMORY MACHINES

1999 ◽  
Vol 10 (04) ◽  
pp. 391-404 ◽  
Author(s):  
KIERAN T. HERLEY ◽  
ANDREA PIETRACAPRINA ◽  
GEPPINO PUCCI
Keyword(s):  
Branch And Bound ◽  
Distributed Memory ◽  
Minimum Cost ◽  
Deterministic Algorithm ◽  
Parallel Computer ◽  
Log P ◽  
Distributed Memory Machines ◽  
Constant Degree ◽  
The Cost ◽  
Ordered Tree

The branch-and-bound problem involves determining the leaf of minimum cost in a cost-labelled, heap-ordered tree, subject to the constraint that only the root is known initially and that the children of a node are revealed only by visiting their parent. We present the first efficient deterministic algorithm to solve the branch-and-bound problem for a tree T of constant degree on a p-procesor distributed-memory Optically Connected Parallel Computer (OCPC). Let c* be the cost of the minimum-cost leaf in T, and let n and h be the number of nodes and the height, respectively, of the subtree T*⊆T of nodes with cost at most c*. When according for both computation and communication costs, our algorithm runs in time O(n/p+h( max {p, log n log p})2) for general values of n, and can be made to run in time O((n/p+h log 4p) log log p) for n polynomial in p. For large ranges of the relevant parameters, our algorithm is provably optimal and improves asymptotically upon the well-known randomized strategy by Karp and Zhang.

A generalized fuzzy cost efficiency model

2020 ◽  
Vol 54 (6) ◽  
pp. 1775-1791
Author(s):  
Nazila Aghayi ◽  
Samira Salehpour
Keyword(s):  
Cost Efficiency ◽  
Minimum Cost ◽  
Extensive Literature ◽  
Data Envelopment ◽  
Fuzzy Environment ◽  
Decision Making Unit ◽  
Production Possibility Set ◽  
Fuzzy Cost ◽  
The Cost ◽  
Generalized Cost

The concept of cost efficiency has become tremendously popular in data envelopment analysis (DEA) as it serves to assess a decision-making unit (DMU) in terms of producing minimum-cost outputs. A large variety of precise and imprecise models have been put forward to measure cost efficiency for the DMUs which have a role in constructing the production possibility set; yet, there’s not an extensive literature on the cost efficiency (CE) measurement for sample DMUs (SDMUs). In an effort to remedy the shortcomings of current models, herein is introduced a generalized cost efficiency model that is capable of operating in a fuzzy environment-involving different types of fuzzy numbers-while preserving the Farrell’s decomposition of cost efficiency. Moreover, to the best of our knowledge, the present paper is the first to measure cost efficiency by using vectors. Ultimately, a useful example is provided to confirm the applicability of the proposed methods.

Main approaches to estimating the cost of shareholder equity of oil and gas producers

2020 ◽  
Vol 26 (3) ◽  
pp. 685-697
Author(s):  
O.V. Shimko
Keyword(s):  
Oil And Gas ◽  
Oil Prices ◽  
Minimum Cost ◽  
Free Cash Flow ◽  
Annual Reports ◽  
Comparative Approach ◽  
Economic Activities ◽  
Advantages And Disadvantages ◽  
Oil And Gas Producers ◽  
The Cost

Subject. The study analyzes generally accepted approaches to assessing the value of companies on the basis of financial statement data of ExxonMobil, Chevron, ConocoPhillips, Occidental Petroleum, Devon Energy, Anadarko Petroleum, EOG Resources, Apache, Marathon Oil, Imperial Oil, Suncor Energy, Husky Energy, Canadian Natural Resources, Royal Dutch Shell, Gazprom, Rosneft, LUKOIL, and others, for 1999—2018. Objectives. The aim is to determine the specifics of using the methods of cost, DFC, and comparative approaches to assessing the value of share capital of oil and gas companies. Methods. The study employs methods of statistical analysis and generalization of materials of scientific articles and official annual reports on the results of financial and economic activities of the largest public oil and gas corporations. Results. Based on the results of a comprehensive analysis, I identified advantages and disadvantages of standard approaches to assessing the value of oil and gas producers. Conclusions. The paper describes pros and cons of the said approaches. For instance, the cost approach is acceptable for assessing the minimum cost of small companies in the industry. The DFC-based approach complicates the reliability of medium-term forecasts for oil prices due to fluctuations in oil prices inherent in the industry, on which the net profit and free cash flow of companies depend to a large extent. The comparative approach enables to quickly determine the range of possible value of the corporation based on transactions data and current market situation.

A claims problem approach to the cost allocation of a minimum cost spanning tree

2021 ◽  
Author(s):  
José-Manuel Giménez-Gómez ◽  
Josep E. Peris ◽  
Begoña Subiza
Keyword(s):  
Spanning Tree ◽  
Cost Allocation ◽  
Minimum Cost ◽  
Claims Problem ◽  
The Cost

scholarly journals Branch and Bound Algorithm Based on Prediction Error of Metamodel for Computational Electromagnetics

Energies ◽  
2020 ◽  
Vol 13 (24) ◽  
pp. 6749
Author(s):  
Reda El Bechari ◽  
Stéphane Brisset ◽  
Stéphane Clénet ◽  
Frédéric Guyomarch ◽  
Jean Claude Mipo
Keyword(s):  
Branch And Bound ◽  
Prediction Error ◽  
Global Solutions ◽  
Black Box ◽  
High Fidelity ◽  
Electromagnetic Devices ◽  
Box Models ◽  
Element Simulation ◽  
The Cost ◽  
Black Box Models

Metamodels proved to be a very efficient strategy for optimizing expensive black-box models, e.g., Finite Element simulation for electromagnetic devices. It enables the reduction of the computational burden for optimization purposes. However, the conventional approach of using metamodels presents limitations such as the cost of metamodel fitting and infill criteria problem-solving. This paper proposes a new algorithm that combines metamodels with a branch and bound (B&B) strategy. However, the efficiency of the B&B algorithm relies on the estimation of the bounds; therefore, we investigated the prediction error given by metamodels to predict the bounds. This combination leads to high fidelity global solutions. We propose a comparison protocol to assess the approach’s performances with respect to those of other algorithms of different categories. Then, two electromagnetic optimization benchmarks are treated. This paper gives practical insights into algorithms that can be used when optimizing electromagnetic devices.

scholarly journals Configurable verification of timed automata with discrete variables

2020 ◽  
Author(s):  
Tamás Tóth ◽  
István Majzik
Keyword(s):  
Timed Automata ◽  
Empirical Evaluation ◽  
Real Time Systems ◽  
Discrete Variables ◽  
Reachability Problem ◽  
Abstraction Refinement ◽  
Dependent Behavior ◽  
Wide Range ◽  
Time Systems ◽  
Lazy Abstraction

AbstractAlgorithms and protocols with time dependent behavior are often specified formally using timed automata. For practical real-time systems, besides real-valued clock variables, these specifications typically contain discrete data variables with nontrivial data flow. In this paper, we propose a configurable lazy abstraction framework for the location reachability problem of timed automata that potentially contain discrete variables. Moreover, based on our previous work, we uniformly formalize in our framework several abstraction refinement strategies for both clock and discrete variables that can be freely combined, resulting in many distinct algorithm configurations. Besides the proposed refinement strategies, the configurability of the framework allows the integration of existing efficient lazy abstraction algorithms for clock variables based on $${\textit{LU}}$$ LU -bounds. We demonstrate the applicability of the framework and the proposed refinement strategies by an empirical evaluation on a wide range of timed automata models, including ones that contain discrete variables or diagonal constraints.

Timetable-Based Transit Assignment Using Branch and Bound Techniques

2001 ◽  
Vol 1752 (1) ◽  
pp. 100-107 ◽  
Author(s):  
Markus Friedrich ◽  
Ingmar Hofsaess ◽  
Steffen Wekeck
Keyword(s):  
Branch And Bound ◽  
Transit Assignment ◽  
Branch And Bound Techniques
Sign in / Sign up

Export Citation Format

Share Document