diff --git a/src/Main.hs b/src/Main.hs
index b95d60a1a146e401c22ba0fa7d249d34c2143251..614e79d460ad3f299b4ab019da626b0264180aa9 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -8,6 +8,7 @@ import System.IO
 import System.Console.GetOpt
 import Control.Monad
 import Control.Applicative ((<$>))
+import Control.Arrow (first)
 import Data.List (partition)
 
 import Parser
@@ -25,7 +26,8 @@ import Solver.SComponent
 
 data InputFormat = PNET | LOLA | TPN deriving (Show,Read)
 
-data NetTransformation = TerminationToReachability
+data NetTransformation = TerminationByReachability
+                       | ValidateIdentifiers
 
 data ImplicitProperty = Termination
                       | NoDeadlock | NoDeadlockUnlessFinal
@@ -68,9 +70,15 @@ options =
         (NoArg (\opt -> Right opt { inputFormat = TPN }))
         "Use the tpn input format"
 
+        , Option "" ["validate-identifiers"]
+        (NoArg (\opt -> Right opt {
+            optTransformations = ValidateIdentifiers : optTransformations opt
+          }))
+        "Make identifiers valid for lola"
+
         , Option "" ["termination-by-reachability"]
         (NoArg (\opt -> Right opt {
-            optTransformations = TerminationToReachability : optTransformations opt
+            optTransformations = TerminationByReachability : optTransformations opt
           }))
         "Prove termination by reducing it to reachability"
 
@@ -191,20 +199,19 @@ placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
 
 transformNet :: (PetriNet, [Property]) -> NetTransformation ->
                (PetriNet, [Property])
-transformNet (net, props) TerminationToReachability =
+transformNet (net, props) TerminationByReachability =
         let prime = ('\'':)
-            primeFst (p,x) = (prime p, x)
             ps = ["'sigma", "'m1", "'m2"] ++
                  places net ++ map prime (places net)
             is = [("'m1", 1)] ++
-                 initials net ++ map primeFst (initials net)
+                 initials net ++ map (first prime) (initials net)
             ts = ("'switch", [("'m1",1)], [("'m2",1)]) :
                  concatMap (\t ->
                     let (preT, postT) = context net t
-                        pre'  = [("'m1",1)] ++ preT  ++ map primeFst preT
-                        post' = [("'m1",1)] ++ postT ++ map primeFst postT
-                        pre''  = ("'m2",1) : map primeFst preT
-                        post'' = [("'m2",1), ("'sigma",1)] ++ map primeFst postT
+                        pre'  = [("'m1",1)] ++ preT  ++ map (first prime) preT
+                        post' = [("'m1",1)] ++ postT ++ map (first prime) postT
+                        pre''  = ("'m2",1) : map (first prime) preT
+                        post'' = [("'m2",1), ("'sigma",1)] ++ map (first prime) postT
                     in  [(t, pre', post'), (prime t, pre'', post'')]
                  )
                  (transitions net)
@@ -212,7 +219,17 @@ transformNet (net, props) TerminationToReachability =
                     foldl (:&:) (Atom (LinIneq (Var "'sigma") Ge (Const 1)))
                       (map (\p -> Atom (LinIneq (Var (prime p)) Ge (Var p)))
                         (places net))
+            -- TODO: map existing liveness properties
         in  (makePetriNetWithTrans (name net) ps ts is, prop : props)
+transformNet (net, props) ValidateIdentifiers =
+        let validate = map (\c -> if c `elem` ",;:(){}\t \n\r" then '_' else c)
+            ps = map validate $ places net
+            ts = map validate $ transitions net
+            is = map (first validate) $ initials net
+            as = map (\(a,b,x) -> (validate a, validate b, x)) $ arcs net
+            net' = makePetriNet (name net) ps ts as is
+            props' = map (rename validate) props
+        in  (net', props')
 
 makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
 makeImplicitProperty _ Termination =
diff --git a/src/PetriNet.hs b/src/PetriNet.hs
index 165247584a78e0fa4605aefeef52751139515d17..e36dce36743d06443e095342a6ce62e3ef7b7a70 100644
--- a/src/PetriNet.hs
+++ b/src/PetriNet.hs
@@ -2,7 +2,7 @@
 
 module PetriNet
     (PetriNet,name,showNetName,places,transitions,initial,
-     pre,lpre,post,lpost,initials,context,
+     pre,lpre,post,lpost,initials,context,arcs,
      makePetriNet,makePetriNetWithTrans)
 where
 
@@ -19,6 +19,10 @@ data PetriNet = PetriNet {
 initial :: PetriNet -> String -> Integer
 initial net p = M.findWithDefault 0 p (initMap net)
 
+arcs :: PetriNet -> [(String, String, Integer)]
+arcs net = concatMap (\(a,(_,bs)) -> map (\(b,w) -> (a,b,w)) bs)
+                           (M.toList (adjacency net))
+
 context :: PetriNet -> String -> ([(String, Integer)], [(String, Integer)])
 context net x = M.findWithDefault ([],[]) x (adjacency net)
 
diff --git a/src/Property.hs b/src/Property.hs
index 3bfd14e22483a981460109b55f34a425254f2596..c6ebde266d940dea4bdff3ba8d95fce0158af14d 100644
--- a/src/Property.hs
+++ b/src/Property.hs
@@ -3,6 +3,7 @@
 module Property
     (Property(..),
      showPropertyName,
+     rename,
      PropertyType(..),
      Formula(..),
      LinearInequation(..),
@@ -25,6 +26,14 @@ instance Show Term where
         show (t :-: u) = "(" ++ show t ++ " - " ++ show u ++ ")"
         show (t :*: u) = show t ++ " * " ++ show u
 
+renameTerm :: (String -> String) -> Term -> Term
+renameTerm f (Var x) = Var (f x)
+renameTerm _ (Const c) = Const c
+renameTerm f (Minus t) = Minus (renameTerm f t)
+renameTerm f (t :+: u) = renameTerm f t :+: renameTerm f u
+renameTerm f (t :-: u) = renameTerm f t :-: renameTerm f u
+renameTerm f (t :*: u) = renameTerm f t :*: renameTerm f u
+
 data Op = Gt | Ge | Eq | Ne | Le | Lt
 
 instance Show Op where
@@ -41,6 +50,10 @@ data LinearInequation = LinIneq Term Op Term
 instance Show LinearInequation where
         show (LinIneq lhs op rhs) = show lhs ++ " " ++ show op ++ " " ++ show rhs
 
+renameLinIneq :: (String -> String) -> LinearInequation -> LinearInequation
+renameLinIneq f (LinIneq lhs op rhs) =
+        LinIneq (renameTerm f lhs) op (renameTerm f rhs)
+
 data Formula = FTrue | FFalse
              | Atom LinearInequation
              | Neg Formula
@@ -58,6 +71,14 @@ instance Show Formula where
         show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
         show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"
 
+renameFormula :: (String -> String) -> Formula -> Formula
+renameFormula _ FTrue = FTrue
+renameFormula _ FFalse = FFalse
+renameFormula f (Atom a) = Atom (renameLinIneq f a)
+renameFormula f (Neg p) = Neg (renameFormula f p)
+renameFormula f (p :&: q) = renameFormula f p :&: renameFormula f q
+renameFormula f (p :|: q) = renameFormula f p :|: renameFormula f q
+
 data PropertyType = Safety | Liveness
 
 instance Show PropertyType where
@@ -74,6 +95,9 @@ instance Show Property where
         show p =
             showPropertyName p ++ " { " ++ show (pformula p) ++ " }"
 
+rename :: (String -> String) -> Property -> Property
+rename f (Property pn pt pf) = Property pn pt (renameFormula f pf)
+
 showPropertyName :: Property -> String
 showPropertyName p = show (ptype p) ++ " property" ++
                (if null (pname p) then "" else " " ++ show (pname p))