The tag has no wiki summary.

learn more… | top users | synonyms

-4
votes
1answer
42 views

Probabilistic protocols [closed]

I want to model a probabilistic protocol using a model checker, but a lot of protocols are already implemented (e.g. Randomised Dining Philosophers, Dining cryptographers, Synchronous leader election ...
3
votes
1answer
41 views

Decidability of membership in the fixed point of a rational relation

Given a finite alphabet $\Sigma$, a non-deterministic finite-state transducer representing rational a relation $T \subseteq \wp(\Sigma^* \times \Sigma^*)$, a finite state machine representing a ...
-4
votes
1answer
54 views

Temporal Logic - Until [closed]

I have a doubt, in Linear Temporal Logic LTL, does the Until operator require that the first occurrence is the first term of the formula? ex: a U b does require ...
0
votes
0answers
28 views

Hoare program correctness

Which is the easiest way to find a valid Invariant for a While Program in the Hoare program correctness verification? Is there a "guided" way to do that?
0
votes
2answers
93 views

LTL property - safety or liveness?

How can I check if an LTL (Linear Temporal Logic) property is safety or liveness? Is it right to say that a property is safety OR liveness (or neither)? How can I evaluate this: ...
2
votes
1answer
131 views

What is the space complexity of CTL model checking?

What is the space complexity of the CTL model checking algorithm via labeling without fairness (see e.g. Model Checking by Clarke at al Section 4.1 or Principles of Model Checking by Baier et al ...
5
votes
1answer
102 views

Logics for timed resource control

I'm studying proof theory and I've seen that linear logic can be used as a way to control resource usage, since by the propositions-as-types it is equivalent to the linear lambda calculus. Is there a ...
2
votes
2answers
87 views

Typechecking liveness properties of coprograms

Clarification: in Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input. I am ...
6
votes
1answer
139 views

Is infinitary logic a logic in the sense of Gurevich?

Gurevich provides an exact definition of what Logic capturing PTIME is. An abstract logic $L$ consists of a set of $L[\tau]$-sentences for each vocabulary $\tau$, and a mapping that maps a property ...
0
votes
0answers
82 views

Given a CSL formula, how can we generate an automaton that accepts the formula?

The problem is same as the title, given a Continous Stochastic Logic(CSL) formula how can we create a machine which accepts the formula? Any intuitive ideas or references will be appreciated.
-1
votes
1answer
83 views

Constructing automata with the same traces, but where a CTL-formula is not equally satisfied [closed]

Hard to put this question in a short title. As part of a self-exercise, I'm trying to solve 6.15b of Principles of Model Checking by Baier and Katoen. You're supposed to prove that there does not ...
1
vote
1answer
219 views

How to show that ECTL* is more expressive than CTL* $\cup$ Büchi (with an example)

I am looking for a preferably simple property that is expressible in ECTL* but not in CTL* and not in Büchi, with a citable reference to the proof. Details of what I've tried: I've tried a ...
9
votes
1answer
396 views

CTL* and mu-calculus

it is well known that the modal $\mu$-calculus is one of the most expressive temporal logics for expressing properties of trees/graphs, and that CTL* is strictly less expressive than the ...
5
votes
1answer
183 views

What is the complexity of model checking Process Logic (LTL fragment)?

Process Logic is a modal logic allowing to reason about temporal properties of programs. Its formulae take the form similar to (Propositional) Dynamic Logic $[P]\phi$, with $P$ being a program (think ...
4
votes
2answers
253 views

Inductive definition of ECTL*: how are recursive formulas forbidden?

In [1], the extended computation tree logic ECTL* is inductively defined as the propositional formulas over all E($A(F_1,..F_n)$), where E is the existential path quantifier and $A$ some Büchi ...
-2
votes
2answers
624 views

Kripke model and LTL vs CTL formulae interpretation [closed]

I have this Kripke model $M$: $$ \begin{array}{ccccccc} \to & (p, q) & \to & (\neg p, \neg q) & \to & (p, \neg q) \\ & \circlearrowright & & & & ...
10
votes
2answers
456 views

Expressiveness of Büchi vs CTL(*)

What is the relationship between the expressiveness of LTL, Büchi/QPTL, CTL and CTL*? Can you give some references that cover as many of these temporal logics as possible (especially between linear- ...
-3
votes
2answers
233 views

Model checking Paxos

I have implemented consensus algorithm (based on Paxos). I have added some random test cases and it seems fine. To be sure, I want to do testing via model checking. I couldn't find a correct article ...
6
votes
1answer
123 views

When we use a proof of unsatisfiability to derive an interpolant, isn't using the interpolant to check satisfiability now redundant?

A few papers I've been reading have algorithms on using interpolants for the following clauses (bounded model checking): $$ \begin{align*} A &= I \wedge T_1 \\ B &= T_2 \wedge T_3 \wedge ...
8
votes
2answers
251 views

Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages)

I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, ...
2
votes
2answers
652 views

Equivalence of two basic blocks

My questions: What are other names for this and similar problems and their fields? ("equivalence of varieties in universal algebra", "equivalence of algebraic structures", "rewriting systems for ...
7
votes
2answers
4k views

What is the difference between LTL and CTL?

I already read examples of formulas in CTL but not in LTL and vice-versa, but I'm having trouble gaining a mental grasp on LTL formulas and really what, at the heart, is the difference.
10
votes
6answers
716 views

A data structure for sets of trees.

Tries allow for efficient storage of lists of elements. The prefixes are shared so it is space efficient. I am looking for a similar way to efficiently store trees. I would like to be able to check ...
6
votes
1answer
205 views

Papers on applying CTL over LTSs

Normally model checking with specifications written in CTL*/CTL is done over Kripke structures, however there are ways of doing it over somehow simpler Labelled Transition Systems, for instance ACTL. ...
7
votes
2answers
331 views

What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?

I'm writing a toy modelchecker, and I'm at the point where it's time to implement LTL to Buchi automata translation. For a variety of obvious reasons, I wish the algorithm to be simple :) e.g. I want ...
16
votes
2answers
969 views

Trace Equivalence vs LTL Equivalence

I am looking for an easy example of two transition systems that are LTL equivalent, but not trace equivalent. I have read the proof of Trace Equivalence being finer than LTL Equivalence in the book ...
13
votes
6answers
553 views

What are practically computable properties of Labelled Transition Systems?

I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would ...
5
votes
1answer
295 views

What is the parameterized complexity of following model checking problem?

Input: Graph $G$ and formula $\varphi_1(\vec x),\varphi_2(\vec x)$ Parameter: $tw(G)+|\varphi_1|+|\varphi_2|$ Problem: Decide if $|\varphi_1(G)|=|\varphi_2(G)|$ where $tw(G)$ is the treewidth ...
10
votes
1answer
222 views

Can someone suggest a recent survey on product form Markov chains?

I'm especially interested in their use in model checking applications. I have Open, Closed and Mixed Networks of Queues with Different Classes of Customers by Baskett et al. Any other suggestions ...