# Tagged Questions

Model checking refers to the following problem: given a model of a system, test automatically whether this model meets a given specification.

34 views

### Can QBF encode #QBF?

In another question Initializing non-deterministic variables in QBF, I was interested about translating assertion-based pseudocode to QBF in order to have an exponentially more compact encoding ...
60 views

### Initializing non-deterministic variables in QBF

I'm trying to translate the following pseudocode to QBF. The integers are encoded as simple fixed-width bitvectors, and the entire procedure runs in polynomial space ensuring QBF has enough ...
21 views

### Complexity of choosing a suitable Boolean algebra domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential non-deterministic program over integer variables, equipped with initial values of these variables. The exact ...
21 views

### Complexity of choosing a suitable positive domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential nondeterministic program over integer variables, equipped with initial values of these variables. The exact ...
36 views

### Complexity of choosing a suitable disjunctive domain for program analysis

Do you know the complexity class of the following problem? Input: A sequential nondeterministic program over integer variables, equipped with initial values of these variables. The exact ...
6 views

### OCL constraints are used to validate/verify instances of meta models. Which (v/v) is true?

I have a meta model of which valid instances are defined by OCL invariants. I'm not sure whether to say that I am validating or verifying instances of that model when I check whether they conform to ...
21 views

### What's the definition of ACTL?

I have been looking for the definition of ACTL, but Google has given me very little to go with. So far, I know ACTL is another form of CTL model checking, and CTL includes the following operators: ...
25 views

### How to prove LTL-formulas true for all paths?

I'm quoting a question from my homework which I don't understand its wording. Also, I'm not looking for an answer for my problem, I just want to be pointed at some articles/tutorials/reading/tips to ...
19 views

### Framework of code generation in model-driven development workflow. Is formal language semantics necessary?

I am implementing worflow where the code in industrial programming languages (JavaScript and Java) should be generated from the formal (formally verified) expressions (from ontologies as objects and ...
18 views

### NuSMV : simple game modeling

I'm new to NuSMV and try to model this simple turn-based game. There are 10 bricks in a pile, each player can take 1-3 brick per turn, whoever take the last brick wins the game. Assume player A go ...
147 views

### LTL properties in bounded model checking via assertions

Is there a way to check LTL properties in a bounded model checker? As an example, consider a liveness property ($G F p$ - always eventually $p$)? Suppose we have the following trivial program ...
54 views

### The Interleaved Transition System for 2 Independent and Concurrent Transition Systems

This question is about Model Checking for Software Formal Verification How do you model the joint behavior of 2 independent and concurrent transition systems? Specifically, given the two independent ...
56 views

### What's a side-effect free expression in Timed Automata?

I'm trying to get myself more familiar with Timed Automata theory. At some point I came across the expression "side-effect free" like in the following: A guard is a side-effect free expression ...
55 views

### What does least fix point and greatest fix point mean in Safety games

In safety games there are these mathematical notation about greatest fix points and least fix points but I don't get it. How would we describe them plain English without mathematical symbols.
52 views

### Determining which states in a transition system satisfy a specific CTL formula [closed]

Trying to answer the following question: However, my answer is that only one of these states satisfy the TS (which is for sure wrong since the next part of this question asks to remove states that ...
71 views

### Find equivalent LTL formula, without Y (Yesterday) operator. How can I handle first state?

The task is to find an equivalent LTL formula for $G(a \Rightarrow Yb)$, which doesn't contain the Y operator. My idea is to search for invalid path patterns with 2 $a$'s in a row, e.g. bbbbaab. ...
85 views

### An algorithm to compute a set of states that satisfy a specific CTL formula

Working through a past exam question and I'm unsure where to start or what form they want the answer in: Define an algorithm that receives as input a finite transition system TS defined over the set ...
106 views

### Given a set of LTL formulas, on which states does the Kripke structure hold? [closed]

I'm currently learning about LTL and CTL formulas and to get a better understanding I try to manually interpret the formulas over a given Kripke structure. Since I'm not 100% sure if my results are ...
84 views

### SPIN / Promela Verification [closed]

I have this code here which performs the 'leader election' among a specified number of processes. In Promela, it is written as: ...
24 views

### A linear temporal property that represents this (basic) execution?

A question gives me a set of atomic propositions AP = {a, b, c}and asks me to give a linear temporal property that represents all executions over AP such that: (1) ...
246 views

### Product of a Transition System and a Finite Automaton

Dealing with a question that asks me to compute the product of the following transition system and finite automaton Can't seem to find a good example on how to do this so I sort of just freestyled ...
61 views