The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Bounded Model Checking (BMC) has been recently introduced as an efficient verification method for reactive systems. BMC based on SAT methods consists in searching for a counterexample of a particular lenght and generating a propositional formula that is satisfiable iff such a counterexample exists. This new technique has been introduced by E.Clarke et al. for model checking of the linear time temporal...
We present an extension of a bounded model checking algorithm to deal with temporal epistemic formulas. We use the algorithm to solve a variant of the bit transmission problem
Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded model checking can be extended to deal with \TACTL\ (the universal fragment of \TCTL ) properties of a network of concurrent Timed Automata.
The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded to the depth k Î N and encoded as a prepositional formula...
The main contribution of the paper consists in showing that the BMC method is feasible for ACTL* (the universal fragment of CTL*) which subsumes both ACTL and LTL. The extension to ACTL* is obtained by redefining the function returning the sufficient number of executions over which an ACTL* formula is checked, and then by combining two known translations to SAT for ACTL and LTL formulas. The proposed...
In this paper we present algorithms for a~Boolean encoding of four basic arithmetic operations on integer numbers: addition, subtraction, multiplication and division. Integer numbers are encoded in two's complement system as vectors of Boolean formulas and arithmetic operations are faithfully encoded as operations on vectors of Boolean formulas. In addition, we also provide an algorithm for a Boolean...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.