diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for LTS
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2020 Ajay Kumar Eeralla
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/LTS.cabal b/LTS.cabal
new file mode 100644
--- /dev/null
+++ b/LTS.cabal
@@ -0,0 +1,66 @@
+name:                LTS
+version:             0.1.0.0
+synopsis:            LTS: Labelled Transition System
+description:         This is an implementation of labelled transition system and
+                     follow the README for information on importing and getting started.
+license:             MIT
+license-file:        LICENSE
+author:              Ajay Kumar Eeralla
+maintainer:          aeeralla@galois.com
+copyright:           ©2020 Ajay Kumar Eeralla
+category:            State Machines
+build-type:          Simple
+cabal-version:       >=1.10
+tested-with:         GHC == 8.2.2
+                     GHC == 8.4.4
+                     GHC == 8.6.5
+                     GHC == 7.10.3
+
+
+extra-source-files:  CHANGELOG.md, README.md
+
+Source-Repository head
+  type:     git
+  location: git@github.com:ajayeeralla/LTS.git
+
+library
+  default-language: Haskell2010
+  hs-source-dirs:   src
+  exposed-modules:
+    Data.LTS
+
+  build-depends:      base >= 4.8.2.0 && <5
+                    , fin >= 0.1.1 && < 0.2
+executable LTS
+  default-language:    Haskell2010
+  build-depends:      LTS
+                    , base                  
+  hs-source-dirs:     programs
+  main-is:            Main.hs
+  ghc-options:        -O2 -fno-warn-unused-do-bind
+
+test-suite lts-tests
+  default-language:   Haskell2010
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     tests
+  main-is:            Main.hs
+  build-depends:      LTS
+                    , QuickCheck ==2.14
+                    , base
+                    , tasty
+                    , tasty-smallcheck
+                    , tasty-hunit
+                    , smallcheck
+  ghc-options:        -O2 -fno-warn-unused-do-bind
+
+benchmark lts-bench
+  default-language:   Haskell2010
+  type:               exitcode-stdio-1.0
+  hs-source-dirs:     bench
+  main-is:            Main.hs
+  build-depends:      LTS
+                    , base
+                    , time
+                    , criterion
+
+  ghc-options:        -O2
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,24 @@
+## LTS: Labelled Transition System
+[![Travis](https://api.travis-ci.com/ajayeeralla/LTS.svg?branch=master)](https://travis-ci.com/github/ajayeeralla/LTS)
+[![MIT license](https://img.shields.io/badge/license-MIT-blue.svg)](https://github.com/ajayeeralla/LTS/edit/master/LICENSE)
+
+This is a library that implements a [labelled transition system](https://en.wikipedia.org/wiki/Transition_system) that can be either deterministic or non-deterministic.
+
+## Example
+
+Here is an example to use LTS library:
+
+```
+import Data.LTS
+
+main = do
+    let s0 :: LTSState Int = LTSState {stateId=0, out=3}
+    let s1 :: LTSState Int = LTSState {stateId=1, out=5}
+    let s2 :: LTSState Int = LTSState {stateId=2, out=7}
+    let t1 :: Transition Int Char = Transition {transitionFrom=s0, transitionGuard='a', transitionTo=s1}
+    let t2 :: Transition Int Char = Transition {transitionFrom=s1, transitionGuard='b', transitionTo=s2}
+
+    putStrLn "depth of LTS [t1, t2]:"
+    print (depth [t1, t2] s0)
+```
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/bench/Main.hs b/bench/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/Main.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main where
+import Criterion.Main
+import Data.LTS
+
+s0 :: LTSState Int = LTSState {stateId=0, out=3}
+s1 :: LTSState Int = LTSState {stateId=1, out=5}
+s2 :: LTSState Int = LTSState {stateId=2, out=7}
+t1 :: Transition Int Char = Transition {transitionFrom=s0, transitionGuard='a', transitionTo=s1}
+t2 :: Transition Int Char = Transition {transitionFrom=s1, transitionGuard='b', transitionTo=s2}
+
+main = defaultMain [
+  bgroup "Depth" [ bench "1"  $ whnf depth [t1]
+                 , bench "5"  $ whnf depth [t1, t2]
+                 ]
+  ]
diff --git a/programs/Main.hs b/programs/Main.hs
new file mode 100644
--- /dev/null
+++ b/programs/Main.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+import Data.LTS
+
+main = do
+    let s0 :: LTSState Int = LTSState {stateId=0, out=3}
+    let s1 :: LTSState Int = LTSState {stateId=1, out=5}
+    let s2 :: LTSState Int = LTSState {stateId=2, out=7}
+    let t1 :: Transition Int Char = Transition {transitionFrom=s0, transitionGuard='a', transitionTo=s1}
+    let t2 :: Transition Int Char = Transition {transitionFrom=s1, transitionGuard='b', transitionTo=s2}
+
+    putStrLn "depth of LTS [t1, t2]:"
+    print (depth [t1, t2] s0)
diff --git a/src/Data/LTS.hs b/src/Data/LTS.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/LTS.hs
@@ -0,0 +1,144 @@
+{- |
+Module      :  Data.LTS
+Description :  A library that models labelled transition system in Haskell
+Copyright   :  Copyright (c) 2020 Ajay Kumar Eeralla
+
+Maintainer  :  ajay.eeralla@gmail.com
+Stability   :  experimental
+Portability :  portable
+
+This module implements a labelled transition system
+-}
+{-# LANGUAGE DeriveGeneric #-}
+
+module Data.LTS
+  ( LTSState (..)
+  , Transition (..)
+  , LTS
+  , checkTrans
+  , getFromIds
+  , getToIds
+  , sortById
+  , sortByToSt
+  , sortByFromSt
+  , collectTrans
+  , getStartSt
+  , getFinalSt
+  , depth
+  , Alphabet
+  , findTransIndex
+  , transExists
+  )
+where
+import Data.Nat
+import GHC.Generics
+import Data.List (sortBy)
+import Data.Ord (comparing)
+
+-- | LTSState is a record type which may hold id, output, etc.
+data LTSState a =
+  LTSState {stateId::Int
+           , out::a
+           }
+           deriving (Read, Show, Eq, Generic)
+
+-- | Define Ord instance by id
+instance (Eq a) => Ord (LTSState a) where
+  compare = comparing stateId
+
+-- | Transition models that on a LTSState, given input symbol from an alphabet [b],
+-- | takes to the next LTSState
+data Transition a b =
+  Transition { transitionFrom::LTSState a
+             , transitionGuard::b
+             , transitionTo::LTSState a
+             }
+             deriving (Read, Show, Eq, Generic)
+
+-- | Define Ord instance for `Transition`
+instance (Eq a, Eq b) => Ord (Transition a b) where
+  compare = comparing transitionFrom
+
+-- | Alphabet is a generic list
+type Alphabet b = [b]
+
+-- | LTS is a list of `Transition`
+type LTS a b = [Transition a b]
+
+-- | Check if transition exists from a given symbol from `Alphabet` and `LTSState`
+transExists :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> Bool
+transExists st x (t:ts) =
+  (transitionFrom t == st && transitionGuard t == x) || transExists st x ts
+
+-- | Return the index of the `Transition` that current state can take on input symbol
+findTransIndex :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> Int
+findTransIndex st x (t:ts) =
+  if transExists st x (t:ts)
+    then index
+    else error "doesn't exist"
+  where index = if transitionFrom t == st && transitionGuard t == x
+                then 0
+                else 1+ findTransIndex st x ts
+
+-- | Return the next state given the input symbol on current `LTSState`
+nextStateSymbol :: (Eq a, Eq b) => LTSState a -> b -> LTS a b -> LTSState a
+nextStateSymbol s x ts =
+  if transExists s x ts
+    then transitionTo (ts !! findTransIndex s x ts)
+    else s
+
+-- | LTS execution on a given state and `Alphabet`
+nextStateAlphabet :: (Eq a, Eq b) => LTSState a -> Alphabet b -> LTS a b -> LTSState a
+nextStateAlphabet s (x:xs) ts =
+  nextStateAlphabet (nextStateSymbol s x ts) xs ts
+
+-- | Check if the set of transitions has same origin
+checkTrans :: (Eq a, Eq b) => LTSState a -> LTS a b -> Bool
+checkTrans st (t:ts) =
+  stateId st == stateId (transitionFrom t) && checkTrans st  ts
+
+-- | Sorting related functions
+-- | Get origin `LTSState` ids
+getFromIds:: (Eq a, Eq b) =>  LTS a b -> [Int]
+getFromIds = map (stateId . transitionFrom)
+
+-- | Get final `LTSState` ids
+getToIds :: (Eq a, Eq b) => LTS a b -> [Int]
+getToIds = map (stateId . transitionTo)
+
+-- | Sort `LTSState`s by Id
+sortById :: (Eq a) => [LTSState a] -> [LTSState a]
+sortById = sortBy (comparing stateId)
+
+-- | Sort transitions by from `LTSState`
+sortByFromSt :: (Eq a, Eq b) => LTS a b -> LTS a b
+sortByFromSt = sortBy (comparing transitionFrom)
+
+-- | Sort transitions by to `LTSState`
+sortByToSt :: (Eq a, Eq b) => LTS a b -> LTS a b
+sortByToSt = sortBy (comparing transitionTo)
+
+-- | Compute set of transitions (that can be ordered using a flag b) from a given `LTSState`
+collectTrans:: (Eq a, Eq b) => LTSState a  -> LTS a b -> Bool -> LTS a b
+collectTrans st (t:ts) b =
+  let op = if stateId st == stateId (transitionFrom t)
+              then t:collectTrans st ts b
+              else collectTrans st ts b
+  in if b then sortByToSt op else op
+
+-- | Get the start `LTSState`
+getStartSt :: (Eq a, Eq b) => LTS a b -> LTSState a
+getStartSt ts =  transitionFrom (head (sortByToSt (sortByFromSt ts)))
+
+-- | Get the final `LTSState`
+getFinalSt :: (Eq a, Eq b) => LTS a b -> LTSState a
+getFinalSt ts =  transitionTo (head (sortByToSt (sortByFromSt ts)))
+
+-- | Compute depth of a transition system which is the longest simple path
+-- | from the start state to a final state
+depth :: (Eq a, Eq b) => LTS a b -> LTSState a -> Nat
+depth [] _ = 0
+depth (t:ts) st
+  | transitionFrom t == st && (transitionFrom t /= transitionTo t) =
+    1 + depth ts (transitionTo t)
+  | otherwise = depth ts st
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Main
+where
+import Test.Tasty
+import Test.Tasty.SmallCheck as SC
+import Test.Tasty.HUnit
+import Data.LTS
+import GHC.Generics
+import Test.SmallCheck.Series
+
+
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Tests" [properties, unitTests]
+
+properties :: TestTree
+properties = testGroup "Properties" [scProps]
+
+instance Serial m a => Serial m (LTSState a)
+instance (Serial m a, Serial m b) => Serial m (Transition a b)
+
+scProps = testGroup "(checked by SmallCheck)"
+    [ SC.testProperty "sortById == sortById . sortById" $
+      \xs -> sortById (xs :: [LTSState Int]) == sortById (sortById xs)
+    ]
+
+s0 :: LTSState Int = LTSState {stateId=0, out=3}
+s1 :: LTSState Int = LTSState {stateId=1, out=5}
+s2 :: LTSState Int = LTSState {stateId=2, out=7}
+t1 :: Transition Int Char = Transition {transitionFrom=s0, transitionGuard='a', transitionTo=s1}
+t2 :: Transition Int Char = Transition {transitionFrom=s1, transitionGuard='b', transitionTo=s2}
+
+unitTests = testGroup "Unit tests"
+  [ testCase "Depth comparison" $
+      depth [t1, t2] s0 `compare` 2 @?= EQ
+  , testCase "Compare transition index" $
+      findTransIndex s0 'a' [t1, t2] `compare` 1 @?= LT
+  , testCase "Check transition Exists" $
+      transExists s1 'b' [t1, t2] `compare` True @?= EQ
+  ]