I am writing a library for a variant of finite automata. States in the automata are named by "keys", which boil down to unsigned ints. For testing purposes, I'd like to be able to test whether two automata are isomorphic -- i.e. they are the same except for perhaps different keys for the corresponding states. (The motivation for this is that there are a few operations like 'determinize' that I don't want to guarantee any particular names for the output states, but I want or need to test something stronger than language equality between the actual and respected result.) One way I've thought of doing this is to convert the transition graph of each automaton to a BGL graph and use it's 'isomorphism' function to determine whether the two are isomorphic. However, I'd need to impose two extra conditions: - Edges between nodes are labeled (with the symbol that makes the automaton take that transition), and I need to make sure these match between the two graphs - Nodes are labeled (with whether they correspond to an initial and accepting state of the automaton), and I need to make sure these match up between the two graphs Does it sound like this task is something the BGL is suited for? Thanks, Evan Driscoll
On Thu, Jun 23, 2011 at 12:28 PM, Evan Driscoll <driscoll@cs.wisc.edu> wrote:
I am writing a library for a variant of finite automata. States in the automata are named by "keys", which boil down to unsigned ints.
For testing purposes, I'd like to be able to test whether two automata are isomorphic -- i.e. they are the same except for perhaps different keys for the corresponding states. (The motivation for this is that there are a few operations like 'determinize' that I don't want to guarantee any particular names for the output states, but I want or need to test something stronger than language equality between the actual and respected result.)
One way I've thought of doing this is to convert the transition graph of each automaton to a BGL graph and use it's 'isomorphism' function to determine whether the two are isomorphic. However, I'd need to impose two extra conditions:
- Edges between nodes are labeled (with the symbol that makes the automaton take that transition), and I need to make sure these match between the two graphs - Nodes are labeled (with whether they correspond to an initial and accepting state of the automaton), and I need to make sure these match up between the two graphs
Hi Evan, The BGL isomorphism-testing implementation lets you pass in vertex invariants that can help you describe your extra conditions. Vertex invariants are mappings f,g that map vertices to integers such that the resulting isomorphism will map vertex u to v if f(u) = g(v). So if you have a vertex u in the first graph that must map to vertex v in the second graph, you can provide f,g such that f(u) = g(v) by mapping your set of labels onto a range of integers. Additionally, if you have an edge (u,v) in the first graph that you want to map to an edge (w,x) in the second graph, just make sure f(u) = g(w) and f(v) = g(x) (I'm assuming your graph is directed since you said it was an automaton.) These invariant mappings default to mappings that return the degree of each vertex in the graph, so you can just replace them with your custom invariants. -Aaron
On 06/23/2011 11:41 AM, Aaron Windsor wrote:
The BGL isomorphism-testing implementation lets you pass in vertex invariants that can help you describe your extra conditions. Vertex invariants are mappings f,g that map vertices to integers such that the resulting isomorphism will map vertex u to v if f(u) = g(v). So if you have a vertex u in the first graph that must map to vertex v in the second graph, you can provide f,g such that f(u) = g(v) by mapping your set of labels onto a range of integers. Additionally, if you have an edge (u,v) in the first graph that you want to map to an edge (w,x) in the second graph, just make sure f(u) = g(w) and f(v) = g(x) (I'm assuming your graph is directed since you said it was an automaton.)
These invariant mappings default to mappings that return the degree of each vertex in the graph, so you can just replace them with your custom invariants.
I saw those in the interface but wasn't sure if that was what I'd need or not. That explanation is not very clear, and sounds incorrect (or at least incomplete). "The resulting isomorphism will map vertex u to v if f(u) = g(v) and ...." what? There've got to be some additional conditions in there relating to connections between the nodes. And because I don't know what it's doing behind the scenes, I can't tell what interface that map *really* provides because the docs don't actually say. For instance, do I need to make sure that the out-degree is encoded in the integer too? I.e. should 'f(v)' encode both the out-degree and initialness/acceptingness of 'v'? And that's not even to the point of trying to figure out a way to encode the edge labels in that scheme; I'm not sure how to do that. I guess maybe I should read that PDF of the algorithm. Maybe that'll help. Evan
On Thu, Jun 23, 2011 at 1:12 PM, Evan Driscoll <driscoll@cs.wisc.edu> wrote:
On 06/23/2011 11:41 AM, Aaron Windsor wrote:
The BGL isomorphism-testing implementation lets you pass in vertex invariants that can help you describe your extra conditions. Vertex invariants are mappings f,g that map vertices to integers such that the resulting isomorphism will map vertex u to v if f(u) = g(v). So if you have a vertex u in the first graph that must map to vertex v in the second graph, you can provide f,g such that f(u) = g(v) by mapping your set of labels onto a range of integers. Additionally, if you have an edge (u,v) in the first graph that you want to map to an edge (w,x) in the second graph, just make sure f(u) = g(w) and f(v) = g(x) (I'm assuming your graph is directed since you said it was an automaton.)
These invariant mappings default to mappings that return the degree of each vertex in the graph, so you can just replace them with your custom invariants.
I saw those in the interface but wasn't sure if that was what I'd need or not. That explanation is not very clear, and sounds incorrect (or at least incomplete).
"The resulting isomorphism will map vertex u to v if f(u) = g(v) and ...." what? There've got to be some additional conditions in there relating to connections between the nodes. And because I don't know what it's doing behind the scenes, I can't tell what interface that map *really* provides because the docs don't actually say.
For instance, do I need to make sure that the out-degree is encoded in the integer too? I.e. should 'f(v)' encode both the out-degree and initialness/acceptingness of 'v'? And that's not even to the point of trying to figure out a way to encode the edge labels in that scheme; I'm not sure how to do that.
You can encode the degree in the mapping, too, and if you do, that will help speed up the isomorphism tester. But you don't have to. The isomorphism tester exhaustively looks for isomorphisms between the two graphs, and the invariants can be used both as hints to speed up the exhaustive search and as ways to enforce actual invariants in the isomorphsim, as you're doing. -Aaron
On 06/23/2011 12:18 PM, Aaron Windsor wrote:
You can encode the degree in the mapping, too, and if you do, that will help speed up the isomorphism tester. But you don't have to. The isomorphism tester exhaustively looks for isomorphisms between the two graphs, and the invariants can be used both as hints to speed up the exhaustive search and as ways to enforce actual invariants in the isomorphsim, as you're doing.
Ah, thanks for this explanation; that makes sense. (That paragraph *really* ought to be in the docs!) I'm looking at the docs for the latest version, and it looks like there was a change at some point from one vertex_invariant to a vertex_invariant1 and vertex_invariant2. Are the docs again unclear on what it does: i.e. vertex_invariant1 behaves as 'f' and is fed vertices from graph1, and vertex_invariant2 behaves as your 'g' and is fed vertices from graph2? Or are they two different invariants just in case you want to do two things? I'm still struggling with the edge label restrictions as well. The only way I can think of to incorporate them is to make sure that the set of labels from corresponding nodes is the same: but that's insufficient: A B (q0) ---------> ((q1)) (p0) ------------> ((p1)) | | | B | A | | V V (q2) (p2) These automata are not isomorphic; they don't even have the same language. But if you can only look at each vertex and the edges that are incident on it, it looks like it is. There may be some clever encoding, but I'm not seeing it... Evan
On 06/23/2011 12:52 PM, Evan Driscoll wrote:
I'm still struggling with the edge label restrictions as well. The only way I can think of to incorporate them is to make sure that the set of labels from corresponding nodes is the same: but that's insufficient:
A B (q0) ---------> ((q1)) (p0) ------------> ((p1)) | | | B | A | | V V (q2) (p2)
These automata are not isomorphic; they don't even have the same language. But if you can only look at each vertex and the edges that are incident on it, it looks like it is.
Actually I lied; you can tell in that case, since q1 <--> p1 by the isomorphism, but the edges incident on q1 is just A and those incident on p1 is just B. But this works to illustrate my point: A B (q0) ---------> ((q1)) (p0) ------------> ((p1)) | /\ | /\ | B | | A | | | B | | A V | V | (q2) (q3) (p2) (p4) /\ /\ | | | A | B | | (q4) (p3) q0, p0 both have no incoming and one A and one B outgoing q1, p1 both have one A and one B incoming and no outgoing q2, p2 both have one A and one B incoming and no outgoing q3, p3 both have one B outgoing and no incoming q4, p4 both have one A outgoing and no incoming Evan
On Thu, 23 Jun 2011, Evan Driscoll wrote:
On 06/23/2011 12:52 PM, Evan Driscoll wrote:
I'm still struggling with the edge label restrictions as well. The only way I can think of to incorporate them is to make sure that the set of labels from corresponding nodes is the same: but that's insufficient:
A B (q0) ---------> ((q1)) (p0) ------------> ((p1)) | | | B | A | | V V (q2) (p2)
These automata are not isomorphic; they don't even have the same language. But if you can only look at each vertex and the edges that are incident on it, it looks like it is.
Actually I lied; you can tell in that case, since q1 <--> p1 by the isomorphism, but the edges incident on q1 is just A and those incident on p1 is just B.
They are isomorphic as graphs, so your original claim was right I think. It looks like edge labels would be difficult to add to the current isomorphism algorithm, though. You could probably get some of the way there by changing the std::vector on line 154 of isomorphism.hpp (in SVN HEAD) to an std::map and passing in a map for invariant1 that returns the sorted list of outgoing edge labels from each vertex. You will probably also need some code to compare the edge labels between two vertices that the algorithm claims should match. That will not handle the more complicated example you put efficiently, though. You would also want to make the DFS order the outgoing edges of each vertex by their labels; there may be other things you need to do as well. I think for now you would be better off rewriting the algorithm, possibly based on the existing one. Contributing it back to BGL would be appreciated if you end up going that way. -- Jeremiah Willcock
OK, I have a somewhat unrelated question. (I think I can modify the Boost algorithm to do what I want.) In libs/graph/example/isomorphism.hpp, if I change undirectedS to bidirectionalS, then the answer changes from the two graphs being isomorphic to not. (It then proceeds to segfault when looking at the isomorphism map.) typedef adjacency_list<vecS, listS, undirectedS, property<vertex_index_t, int> > graph_t; to typedef adjacency_list<vecS, listS, bidirectionalS, property<vertex_index_t, int> > graph_t; Why is this? Near as I can tell, the graphs should be isomorphic. Graph 1 has three cycles, 0->1->2->0, 3->4->5->6->3, and 7->8->9->10->11->7. Graph 2 has three cycles of the same sizes, 9->10->11->9, 0->1->3->2->0, and 4->5->7->8->6->4. (These are all the transitions.) Evan Driscoll
On 06/23/2011 08:28 PM, Evan Driscoll wrote:
In libs/graph/example/isomorphism.hpp, if I change undirectedS to bidirectionalS, then the answer changes from the two graphs being isomorphic to not. (It then proceeds to segfault when looking at the isomorphism map.)
BTW, I've tried this on Boost 1.33.1 (extremely old, I know) and 1.47 beta. So unless it was fixed then broken... :-) Evan
On Thu, 23 Jun 2011, Evan Driscoll wrote:
OK, I have a somewhat unrelated question. (I think I can modify the Boost algorithm to do what I want.)
In libs/graph/example/isomorphism.hpp, if I change undirectedS to bidirectionalS, then the answer changes from the two graphs being isomorphic to not. (It then proceeds to segfault when looking at the isomorphism map.)
typedef adjacency_list<vecS, listS, undirectedS, property<vertex_index_t, int> > graph_t; to typedef adjacency_list<vecS, listS, bidirectionalS, property<vertex_index_t, int> > graph_t;
Why is this?
Near as I can tell, the graphs should be isomorphic. Graph 1 has three cycles, 0->1->2->0, 3->4->5->6->3, and 7->8->9->10->11->7. Graph 2 has three cycles of the same sizes, 9->10->11->9, 0->1->3->2->0, and 4->5->7->8->6->4. (These are all the transitions.)
They are not isomorphic as directed graphs: the first component in g1 is 0->1, 1->2, 0->2 (acyclic), while the first component in g2 is 9->10, 10->11, 11->9 (a cycle). The other components are isomorphic in the way that you show. -- Jeremiah Willcock
On 06/23/2011 08:37 PM, Jeremiah Willcock wrote:
They are not isomorphic as directed graphs: the first component in g1 is 0->1, 1->2, 0->2 (acyclic), while the first component in g2 is 9->10, 10->11, 11->9 (a cycle). The other components are isomorphic in the way that you show.
Oh, duh. Too careless. Thanks, Evan
participants (6)
-
Aaron Windsor -
Evan Driscoll -
Jeremiah Willcock