I was wondering if it is possible to have consensus or to formalize general definition of reachability property in graphs. If yes then what can be its fragments?
For instance: If I say that following are sufficiently enough to define reachability would it be correct by construction? or any way to formally proof that these are necessary and sufficient conditions.
Property 1: No self connectivity: fragments should not be connected to themselves to avoid infinite length cycles in a kirpke structure.
Property 2:Link connectivity: 2 fragments or elements of the graph are reachable if they have link connectivity.
property 3: Fixing source and destination, to avoid all other interpretations of logical reachability.
property 4: Fix the length of bounds: by fixing the number of intermediate nodes or fragments.
PS: please do not confuse bounded reachability with bounded model checking.
I have also uploaded the formal description of properties. Which one are necessary and sufficient and is there a way to prove that they are necessary and sufficient?
Peter thanks for responding, but this is not what I want. I am referring to simple formal definition of bounded reachability. In which I can fix the number on intermediate nodes, and check whether a source is able to reach a destination or not, given link connectivity requirements.
Peter, I presume you might have not read my main post clearly. I have mentioned not to confuse bounded reachability of graph, with bounded model checking (in which we can verify whether certain state is reachable in k-transitions/steps or not).
Psi3 is not at all nonsense. It ensures that: all interpretations of uninterpreted function P(x,y) (which means reachability between x and y) should be avoided in which x is not the source and y is not destination. This is to make search efficient, and avoid hundreds or perhaps thousands of undesired interpretations.Psi4 explains and puts bound over the length of reachability.
My question was not as you took it. I want to prove which of these: Psi_{i} are necessary and sufficient for bounded reachability (between a source and destination given a graph).
Does it make sense?
As far as you definition is concerned, its not clear where is reachability? as I am not an expert of modal logic. Perhaps I should not have mentioned Kirpke structure... By bounded reachability I meant, to fix the number of intermediate nodes/point between source and destination, or in short to fix the length of reachability.
but still the main point is missing, how to prove whether set of properties in this case are necessary and sufficient to capture the dynamics of so called bounded reachability....
It is intuitive but just for your understanding: x and y are reachable if the following properties hold true.
P(x,y): True -> Psi1 /\ Psi2 /\ Psi3 /\ Psi4
where L(x,y) is link/logical connectivity of graph which determines the neighboring entities. In conjunction yes they come under universal quantification, that's why they do makes sense.
Still if it doesn't make any sense to you.... perhaps you should give others a chance to respond.....
Peter,
I appriciate your effort for explanation but I could not understand anything about your last comment. All I am looking for is the proof, that the constraints/formalism I have is sufficient, sound and complete to find path of length 4 (which means maximum 3 intermediate nodes should be considered for reachability from source to destination). If they are not sufficient then what is missing? or what is extra? what is not necessary?
:) actually my goal is to find a satisfiable solution, and to formalize generalized definition. I will fix x and y and SAT/SMT solvers using this definition can check whether there exists any path between x and y or not. Now the problem is to theoretically prove the soundness of properties. The closest thing I could figure out which makes sense to me (or which I could understand is the following part of your first comment): So lets take it and start from there.
"
So wouldn't that be q->p\/Op\/O2p\/...\/ONp for arbitrary (nonempty) p,q? And since the difficult part is when q is as large as possible, that seems to boil down to p\/Op\/O2p\/...\/ONp being true whenever not p is not true :-). I.e. ~p\/p\/Op\/O2p\/...\/ONp is true.
"
Set of nodes in a graph is fixed: lets assume it your way as a set of "starting strings" (all possible sources): p, now domain of p is |N, and set of termination strings (all possible destinations) is: q, whose domain is also |N (set of natural number). Now when you say: q- > pVOpVO^2pV....O^n P, what does exactly this means in terms of nodes/graph? because my goal is to correctly prove that there exist a set of intermediate nodes R: which is a subset p, which can be found using my formalism.
For this purpose, there is another set "PEER" which is also sub set of p and R intersection PEER= {emptyset}, which means strings or nodes \in R, which are helping connect a certain set of source and destination \in PEER, should not be the same, to avoid self loops. now how to prove that under given constraints/properties of assumptions we can find all possible paths of length 3 for all pairs of source and destination. Does it makes sense?
Reachability from a to b means the existence of a finite sequence a1, a2, ... an such that E(a, a1) and E(a1, a2) and ... and E(an, b). This property is not first order definable, but is definable in FO + LFP. Consequently, it can be checked in polynomial time!
FO = first order, LFP = least fix point; for the logic LO + LFP and how it defines reachability, see the book Descriptive Complexity by Immerman:
http://www.springer.com/us/book/9780387986005
- Badges
- Science topic
- Similar topics
- Mathematical Sciences
- Graphs