共查询到20条相似文献,搜索用时 31 毫秒
1.
Model Checking with Strong Fairness 总被引:1,自引:0,他引:1
In this paper we present a coherent framework for symbolic model checking of linear-time temporal logic (ltl) properties over finite state reactive systems, taking full fairness constraints into consideration. We use the computational
model of a fair discrete system (fds) which takes into account both justice (weak fairness) and compassion (strong fairness). The approach presented here reduces the model-checking problem into the question of whether a given fds is feasible (i.e. has at least one computation).
The contribution of the paper is twofold: On the methodological level, it presents a direct self-contained exposition of full
ltl symbolic model checking without resorting to reductions to either μ-calculus or ctl. On the technical level, it extends previous methods by dealing with compassion at the algorithmic level instead of either
adding it to the specification, or transforming compassion to justice.
Finally, we extend ctl∗ with past operators, and show that the basic symbolic feasibility algorithm presented here, can be used to model check an
arbitrary ctl∗ formula over an fds with full fairness constraints.
This research was supported in part by an infra-structure grant from the Israeli Ministry of Science and Art, a grant from
the U.S.-Israel Binational Science Foundation, and a gift from Intel. 相似文献
2.
Temporal logics are commonly used for reasoning about concurrent systems. Model checkers and other finite-state verification
techniques allow for automated checking of system model compliance to given temporal properties. These properties are typically
specified as linear-time formulae in temporal logics. Unfortunately, the level of inherent sophistication required by these
formalisms too often represents an impediment to move these techniques from “research theory” to “industry practice”. The
objective of this work is to facilitate the nontrivial and error prone task of specifying, correctly and without expertise
in temporal logic, temporal properties.
In order to understand the basis of a simple but expressive formalism for specifying temporal properties we critically analyze
commonly used in practice visual notations. Then we present a scenario-based visual language called Property Sequence Chart
(PSC) that, in our opinion, fixes the highlighted lacks of these notations by extending a subset of UML 2.0 Interaction Sequence Diagrams. We also provide PSC with both denotational and operational semantics. The operational semantics is obtained via translation into Büchi automata
and the translation algorithm is implemented as a plugin of our Charmy tool. Expressiveness of PSC has been validated with respect to well known property specification patterns.
Preliminary results appeared in (Autili et al. 2006a). 相似文献
3.
Planning for temporally extended goals 总被引:2,自引:0,他引:2
Fahiem Bacchus Froduald Kabanza 《Annals of Mathematics and Artificial Intelligence》1998,22(1-2):5-27
In planning, goals have traditionally been viewed as specifying a set of desirable final states. Any plan that transforms
the current state to one of these desirable states is viewed to be correct. Goals of this form are limited in what they can
specify, and they also do not allow us to constrain the manner in which the plan achieves its objectives. We propose viewing
goals as specifying desirable sequences of states, and a plan to be correct if its execution yields one of these desirable
sequences. We present a logical language, a temporal logic, for specifying goals with this semantics. Our language is rich
and allows the representation of a range of temporally extended goals, including classical goals, goals with temporal deadlines,
quantified goals (with both universal and existential quantification), safety goals, and maintenance goals. Our formalism
is simple and yet extends previous approaches in this area. We also present a planning algorithm that can generate correct
plans for these goals. This algorithm has been implemented, and we provide some examples of the formalism at work. The end
result is a planning system which can generate plans that satisfy a novel and useful set of conditions.
This revised version was published online in June 2006 with corrections to the Cover Date. 相似文献
4.
We study the problem of guaranteeing correct execution semantics in parallel implementations of logic programming languages in presence of built-in constructs that are sensitive to order
of execution. The declarative semantics of logic programming languages permit execution of various goals in any arbitrary
order (including in parallel). However, goals corresponding to extra-logical built-in constructs should respect the sequential
order of execution to ensure correct semantics. Ensuring this correctness in presence of such built-in constructs, while efficiently
exploiting maximum parallelism, is a difficult problem. In this paper, we propose a formalization of this problem in terms
of operations on dynamic trees. This abstraction enables us to: (i) show that existing schemes to handle order-sensitive computations used in current parallel
systems are sub-optimal; (ii) develop a novel, optimal scheme to handle order-sensitive goals that requires only a constant time overhead per operation. While we present our results in the context of logic programming, they will apply equally well to
most parallel non-deterministic systems.
Received: 20 April 1998 / 3 April 2000 相似文献
5.
Patricia Bouyer Thomas Brihaye Véronique Bruyère Jean-François Raskin 《Formal Methods in System Design》2007,31(2):135-175
We study the cost-optimal reachability problem for weighted timed automata such that positive and negative costs are allowed
on edges and locations. By optimality, we mean an infimum cost as well as a supremum cost. We show that this problem is PSpace-Complete. Our proof uses techniques of linear programming, and thus exploits an important property of optimal runs: their time-transitions
use a time τ which is arbitrarily close to an integer. We then propose an extension of the region graph, the weighted discrete graph,
whose structure gives light on the way to solve the cost-optimal reachability problem. We also give an application of the
cost-optimal reachability problem in the context of timed games.
Research supported by the FRFC project “Centre Fédéré en Vérification” funded by the Belgian National Science Foundation (FNRS)
under grant nr 2.4530.02. 相似文献
6.
The software model checker Blast 总被引:2,自引:0,他引:2
Dirk Beyer Thomas A. Henzinger Ranjit Jhala Rupak Majumdar 《International Journal on Software Tools for Technology Transfer (STTT)》2007,9(5-6):505-525
Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal
safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation
of the property (or, since the problem is undecidable, does not terminate). Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based
predicate discovery. This paper gives an introduction to Blast and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the
first case study, we use Blast to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations.
Then, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution
scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use Blast to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and
a target predicate p, Blast determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that Blast can provide automated, precise, and scalable analysis for C programs. 相似文献
7.
一类扩展的动态描述逻辑 总被引:4,自引:0,他引:4
作为描述逻辑的扩展,动态描述逻辑为语义Web服务的建模和推理提供了一种有效途径.在将语义Web服务建模为动作之后,动态描述逻辑从动作执行结果的角度提供了丰富的推理机制,但对于动作的执行过程却不能加以处理.借鉴Pratt关于命题动态逻辑的相关研究,一方面,对动态描述逻辑中动作的语义重新进行定义,将每个动作解释为由关于可能世界的序列组成的集合;另一方面,在动态描述逻辑中引入动作过程断言,用来对动作的执行过程加以刻画.在此基础上提出一类扩展的动态描述逻辑EDDL(X),其中的X表示从ALC(attributive language with complements)到SHOIN(D)等具有不同描述能力的描述逻辑.以X为描述逻辑ALCQO(attributive language with complements,qualified number restrictions and nominals)的情况为例,给出了EDDL(ALCQO)的表判定算法,并证明了算法的可终止性、可靠性和完备性.EDDL(X)可以从动作执行过程和动作执行结果两个方面对动作进行全面的刻画和推理,为语义Web服务的建模和推理提供了进一步的逻辑支持. 相似文献
8.
Agents are an important technology that have the potential to take over contemporary methods for analysing, designing, and
implementing complex software. The Belief-Desire-Intention (BDI) agent paradigm has proven to be one of the major approaches
to intelligent agent systems, both in academia and in industry. Typical BDI agent-oriented programming languages rely on user-provided
“plan libraries” to achieve goals, and online context sensitive subgoal selection and expansion. These allow for the development of systems that are extremely flexible
and responsive to the environment, and as a result, well suited for complex applications with (soft) real-time reasoning and
control requirements. Nonetheless, complex decision making that goes beyond, but is compatible with, run-time context-dependent
plan selection is one of the most natural and important next steps within this technology. In this paper we develop a typical
BDI-style agent-oriented programming language that enhances usual BDI programming style with three distinguished features:
declarative goals, look-ahead planning, and failure handling. First, an account that mixes both procedural and declarative aspects of goals is necessary in order to reason about important
properties of goals and to decouple plans from what these plans are meant to achieve. Second, lookahead deliberation about
the effects of one choice of expansion over another is clearly desirable or even mandatory in many circumstances so as to
guarantee goal achievability and to avoid undesired situations. Finally, a failure handling mechanism, suitably integrated
with both declarative goals and planning, is required in order to model an adequate level of commitment to goals, as well
as to be consistent with most real BDI implemented systems. 相似文献
9.
Matthias Hecking 《Artificial Intelligence Review》2000,14(3):153-180
We have realized the help system SINIX Consultant (SC) for SINIX1 users. The system is capable of answering – in German – natural language questions concerning SINIX commands, objects, and
concepts. But not only does this help system react to inquiries – additionally, the system is capable of activating itself.
If the user employs a sequence of SINIX commands (a plan) in order to reach a specific goal, the help system proposes a sequence
which reaches the same goal, but, with fewer commands. In this paper, a brief survey of the SINIX Consultant and the realized
plan recognizer REPLIX is first given. Then, an initial attempt of a theoretical treatment of plan recognition is presented.
This is done within the logical framework. We show how we can use an interval-based logic of time to describe actions, atomic
plans, non-atomic plans, action execution, and simple plan recognition. We also show that the recognition of inserted sub-plans
managed by REPLIX can be handled as well. Then, we present a problem which cannot be treated in the formalism. Thus, in this
paper, we don't present a full developed theory but nevertheless, a step towards it.
This revised version was published online in August 2006 with corrections to the Cover Date. 相似文献
10.
Two base algorithms are known for reachability verification over timed automata. They are called forward and backwards, and traverse the automata edges using either successors or predecessors. Both usually work with a data structure called Difference Bound Matrices (DBMs). Although forward is better suited for on-the-fly construction of the model, the one known as backwards provides the basis for the verification of arbitrary formulae of the TCTL logic, and more importantly, for controller synthesis. Zeus is a distributed model checker for timed automata that uses the backwards algorithm. It works assigning each automata location to only one processor. This design choice seems the only reasonable way to deal with some complex operations involving many DBMs in order to avoid huge overheads due to distribution. This article explores the limitations of Zeus-like approaches for the distribution of timed model checkers.Our findings justify why close-to-linear speedups are so difficult –and sometimes impossible– to achieve in the general case. Nevertheless, we present mechanisms based on the way model checking is usually applied. Among others, these include model-topology-aware partitioning and on-the-fly workload redistribution. Combined, they have a positive impact on the speedups obtained.
相似文献
F. SchapachnikEmail: |
11.
Propositional satisfiability (SAT) is a success story in Computer Science and Artificial Intelligence: SAT solvers are currently
used to solve problems in many different application domains, including planning and formal verification. The main reason
for this success is that modern SAT solvers can successfully deal with problems having millions of variables. All these solvers
are based on the Davis–Logemann–Loveland procedure (dll). In its original version, dll is a decision procedure, but it can be very easily modified in order to return one or all assignments satisfying the input
set of clauses, assuming at least one exists. However, in many cases it is not enough to compute assignments satisfying all
the input clauses: Indeed, the returned assignments have also to be “optimal” in some sense, e.g., they have to satisfy as
many other constraints—expressed as preferences—as possible. In this paper we start with qualitative preferences on literals,
defined as a partially ordered set (poset) of literals. Such a poset induces a poset on total assignments and leads to the
definition of optimal model for a formula ψ as a minimal element of the poset on the models of ψ. We show (i) how dll can be extended in order to return one or all optimal models of ψ (once converted in clauses and assuming ψ is satisfiable), and (ii) how the same procedures can be used to compute optimal models wrt a qualitative preference on formulas and/or wrt a quantitative
preference on literals or formulas. We implemented our ideas and we tested the resulting system on a variety of very challenging
structured benchmarks. The results indicate that our implementation has comparable performances with other state-of-the-art
systems, tailored for the specific problems we consider. 相似文献
12.
This paper proposes a predicate nameddosim which provides a new function for parallel execution of logic programs. The parallelism achieved by this predicate is a simultaneous
mapping operation such as bagof and setof predicates. However, the degree of parallelism can be easily decided by arranging
the arguments of the dosim goal. The parallel processing system with dosim was realized on a tight-coupled multiprocessor
machine. To control the degree of parallelism and reduce the amount of memory required for execution, we introduce the grouping
method for the goals executed in parallel and some variations of the dosim predicate. The effectiveness of the proposed method
is demonstrated by the results of the execution of several applications. 相似文献
13.
Abstract. Processor speed and memory capacity are increasing several times faster than disk speed. This disparity suggests that disk
I/ O performance could become an important bottleneck. Methods are needed for using disks more efficiently. Past analysis of
disk scheduling algorithms has largely been experimental and little attempt has been made to develop algorithms with provable
performance guarantees.
We consider the following disk scheduling problem. Given a set of requests on a computer disk and a convex reachability function
that determines how fast the disk head travels between tracks, our goal is to schedule the disk head so that it services all
the requests in the shortest time possible. We present a 3/2 -approximation algorithm (with a constant additive term). For the special case in which the reachability function is linear
we present an optimal polynomial-time solution.
The disk scheduling problem is related to the special case of the Asymmetric Traveling Salesman Problem with the triangle
inequality (ATSP-Δ ) in which all distances are either 0 or some constant α . We show how to find the optimal tour in polynomial time and describe how this gives another approximation algorithm for
the disk scheduling problem. Finally we consider the on-line version of the problem in which uniformly distributed requests
arrive over time. We present an algorithm related to the above ATSP-Δ . 相似文献
14.
Symbolic computational techniques for solving games 总被引:1,自引:0,他引:1
Rajeev Alur P. Madhusudan Wonhong Nam 《International Journal on Software Tools for Technology Transfer (STTT)》2005,7(2):118-128
Games are useful in modular specification and analysis of systems where the distinction among the choices controlled by different components (for instance, the system and its environment) is made explicit. In this paper, we formulate and compare various symbolic computational techniques for deciding the existence of winning strategies. The game structure is given implicitly, and the winning condition is either a reachability game of the form p until q (for state predicates p and q) or a safety game of the form Always p.For reachability games, the first technique employs symbolic fixed-point computation using ordered binary decision diagrams (BDDs) [9]. The second technique checks for the existence of strategies that ensure winning within k steps, for a user-specified bound k, by reduction to the satisfiability of quantified boolean formulas. Finally, the bounded case can also be solved by reduction to satisfiability of ordinary boolean formulas, and we discuss two techniques, one based on encoding the strategy tree and one based on encoding a witness subgraph, for reduction to Sat. We also show how some of these techniques can be adopted to solve safety games. We compare the various approaches by evaluating them on two examples for reachability games, and on an interface synthesis example for a fragment of TinyOS [15] for safety games. We use existing tools such as Mocha [4], Mucke [7], Semprop [19], Qube [12], and Berkmin [13] and contrast the results. 相似文献
15.
Ji?�� Rach?nek Dana ?alounov�� 《Soft Computing - A Fusion of Foundations, Methodologies and Applications》2011,15(1):199-203
Bounded residuated lattice ordered monoids (RlR\ell-monoids) are a common generalization of pseudo-BLBL-algebras and Heyting algebras, i.e. algebras of the non-commutative basic fuzzy logic (and consequently of the basic fuzzy
logic, the Łukasiewicz logic and the non-commutative Łukasiewicz logic) and the intuitionistic logic, respectively. We investigate
bounded RlR\ell-monoids satisfying the general comparability condition in connection with their states (analogues of probability measures).
It is shown that if an extremal state on Boolean elements fulfils a simple condition, then it can be uniquely extended to
an extremal state on the RlR\ell-monoid, and that if every extremal state satisfies this condition, then the RlR\ell-monoid is a pseudo-BLBL-algebra. 相似文献
16.
Answer set programming (ASP) emerged in the late 1990s as a new logic programming paradigm that has been successfully applied
in various application domains. Also motivated by the availability of efficient solvers for propositional satisfiability (SAT),
various reductions from logic programs to SAT were introduced. All these reductions, however, are limited to a subclass of
logic programs or introduce new variables or may produce exponentially bigger propositional formulas. In this paper, we present
a SAT-based procedure, called ASPSAT, that (1) deals with any (nondisjunctive) logic program, (2) works on a propositional
formula without additional variables (except for those possibly introduced by the clause form transformation), and (3) is
guaranteed to work in polynomial space. From a theoretical perspective, we prove soundness and completeness of ASPSAT. From
a practical perspective, we have (1) implemented ASPSAT in Cmodels, (2) extended the basic procedures in order to incorporate the most popular SAT reasoning strategies, and (3) conducted an
extensive comparative analysis involving other state-of-the-art answer set solvers. The experimental analysis shows that our
solver is competitive with the other solvers we considered and that the reasoning strategies that work best on ‘small but
hard’ problems are ineffective on ‘big but easy’ problems and vice versa. 相似文献
17.
We study a family of problems, called Maximum Solution (Max Sol), where the objective is to maximise a linear goal function over the feasible integer assignments to a set of variables subject
to a set of constraints. When the domain is Boolean (i.e. restricted to {0,1}), the maximum solution problem is identical
to the well-studied Max Ones problem, and the complexity and approximability is completely understood for all restrictions on the underlying constraints.
We continue this line of research by considering the Max Sol problem for relations defined by regular signed logic over finite subsets of the natural numbers; the complexity of
the corresponding decision problem has recently been classified by Creignou et al. (Theory Comput. Syst. 42(2):239–255, 2008). We give sufficient conditions for when such problems are polynomial-time solvable and we prove that they are APX-hard otherwise. Similar dichotomies are also obtained for variants of the Max Sol problem. 相似文献
18.
Alternating-time temporal logic (atl) is a logic for reasoning about open computational systems and multi-agent systems. It is well known that atl model checking is linear in the size of the model. We point out, however, that the size of an atl model is usually exponential in the number of agents. When the size of models is defined in terms of states and agents rather than transitions, it turns out that the problem is (1) Δ
3
P
-complete for concurrent game structures, and (2) Δ
2
P
-complete for alternating transition systems. Moreover, for “Positive atl” that allows for negation only on the level of propositions, model checking is (1) Σ
2
P
-complete for concurrent game structures, and (2) NP-complete for alternating transition systems. We show a nondeterministic polynomial reduction from checking arbitrary alternating
transition systems to checking turn-based transition systems, We also discuss the determinism assumption in alternating transition
systems, and show that it can be easily removed.
In the second part of the paper, we study the model checking complexity for formulae of atl
with imperfect information (atl
ir
). We show that the problem is Δ
2
P
-complete in the number of transitions and the length of the formula (thereby closing a gap in previous work of Schobbens
in Electron. Notes Theor. Comput. Sci. 85(2), 2004). Then, we take a closer look and use the same fine structure complexity measure as we did for atl with perfect information. We get the surprising result that checking formulae of atl
ir
is also Δ
3
P
-complete in the general case, and Σ
2
P
-complete for “Positive atl
ir
”. Thus, model checking agents’ abilities for both perfect and imperfect information systems belongs to the same complexity
class when a finer-grained analysis is used. 相似文献
19.
Mathijs de Weerdt André Bos Hans Tonino Cees Witteveen 《Annals of Mathematics and Artificial Intelligence》2003,37(1-2):93-130
In a multi-agent system, agents are carrying out certain tasks by executing plans. Consequently, the problem of finding a plan, given a certain goal, has been given a lot of attention in the literature. Instead of concentrating on this problem, the focus of this paper is on cooperation between agents which already have constructed plans for their goals. By cooperating, agents might reduce the number of actions they have to perform in order to fulfill their goals. The key idea is that in carrying out a plan an agent possibly produces side products that can be used as resources by other agents. As a result, an other agent can discard some of its planned actions. This process of exchanging products, called plan merging, results in distributed plans in which agents become dependent on each other, but are able to attain their goals more efficiently. In order to model this kind of cooperation, a new formalism is developed in which side products are modeled explicitly. The formalism is a resource logic based on the notions of resource, skill, goal, and service. Starting with some resources, an agent can perform a number of skills in order to produce other resources which suffice to achieve some given goals. Here, a skill is an elementary production process taking as inputs resources satisfying certain constraints. A service is a serial or parallel composition of skills acting as a program. An operational semantics is developed for these services as programs. Using this formalism, an algorithm for plan merging is developed, which is anytime and runs in polynomial time. Furthermore, a variant of this algorithm is proposed that handles the exchange of resources in a more flexible way. The ideas in the paper will be illustrated by an example from public transportation. 相似文献
20.
This is the second of two related papers. In “Revising Z: Part I - logic and semantics” (this journal) we introduced a simple
specification logic Z
C
comprising a logic and a semantics (in ZF set theory). We then provided an interpretation for (a rational reconstruction
of) the specification language Z within Z
C
. As a result we obtained a sound logic for Z, including the basic schema calculus. In this paper we extend the basic framework
with more sophisticated features (including schema operations) and we mount a critique of a number of concepts used in Z.
We further demonstrate that the complications and confusions which these concepts introduce can be avoided without compromising
expressibility.
Received March 1998 / Accepted in revised form April 1999 相似文献