diff --git a/NEWS b/NEWS
index 8e0f8d5e7..1b279245e 100644
--- a/NEWS
+++ b/NEWS
@@ -48,6 +48,10 @@ New in spot 1.99.5a (not yet released)
     automata already tagged as "deterministic", and "inherently-weak"
     or "weak" even for automata tagged "weak" or "terminal".
 
+  * The HOA printer has a new option "k" (use "-Hk" from the command
+    line) to output automata using state labels whenever possible.
+    This is useful to print Kripke structures.
+
   * The dot output will display pair of states when displaying an
     automaton built as an explicit product.  This works in IPython
     with spot.product() or spot.product_or() and in the shell with
diff --git a/doc/org/hoa.org b/doc/org/hoa.org
index 9601f0344..69fb730e9 100644
--- a/doc/org/hoa.org
+++ b/doc/org/hoa.org
@@ -510,6 +510,79 @@ Acceptance: 6 (Fin(0)|Fin(1)) | (Fin(2) & Fin(3) & (Inf(4)&Inf(5)))
 Here =Fin(0)|Fin(1)= is actually a single internal term =Fin({0,1})=,
 and likewise for =Inf(4)&Inf(5)=.
 
+** State-based vs. transition-based labels
+
+State labels are handled in the same way as state-based acceptance:
+Spot store labels on transitions internally, so if an input automaton
+has state labels, those are pushed to all outgoing transitions.
+
+For instance an automaton declared in some HOA file with this body:
+
+#+BEGIN_SRC sh :results silent :exports results
+cat >stvstrlab.hoa <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "p0" "p1"
+Acceptance: 1 Inf(1)
+--BODY--
+State: [0&1] 0
+0 1 2
+State: [!0&1] 1 {0}
+0 1
+State: [!1] 2
+2 1
+--END--
+EOF
+#+END_SRC
+
+#+RESULTS:
+
+#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
+sed -n '/--BODY/,/--END/p' stvstrlab.hoa | grep -v -- --
+#+END_SRC
+
+#+RESULTS:
+#+BEGIN_SRC hoa
+State: [0&1] 0
+0 1 2
+State: [!0&1] 1 {0}
+0 1
+State: [!1] 2
+2 1
+#+END_SRC
+
+will always be stored as an automaton with the following transition
+structure
+
+
+#+BEGIN_SRC sh :results verbatim :exports results :wrap SRC hoa
+autfilt -Ht stvstrlab.hoa | sed -n '/--BODY/,/--END/p' | grep -v -- --
+#+END_SRC
+
+#+RESULTS:
+#+BEGIN_SRC hoa
+State: 0
+[0&1] 0
+[0&1] 1
+[0&1] 2
+State: 1
+[!0&1] 0 {0}
+[!0&1] 1 {0}
+State: 2
+[!1] 2
+[!1] 1
+#+END_SRC
+
+#+BEGIN_SRC sh :results silent :exports results
+rm -f stvstrlab.hoa
+#+END_SRC
+
+The HOA printer has an option to output automata using state-based
+labels whenever that is possible.  The option is named =k= (i.e., use
+=-Hk= with command-line tools) because it is useful when the HOA file
+is used to describe a Kripke structure.
+
 ** Property bits
 
 The =HOA= format supports a number of optional =property:= tokens.
@@ -577,24 +650,24 @@ particular:
   to detect deterministic automata that have been output by algorithms
   that do not try to output deterministic automata.
 
-| property            | parser  | stored | printer                                     | notes                                                  |
-|---------------------+---------+--------+---------------------------------------------+--------------------------------------------------------|
-| =state-labels=      | checked | no     | never                                       | state labels are always converted to transition labels |
-| =trans-labels=      | checked | no     | always, unless =-Hi=                        |                                                        |
-| =implicit-labels=   | checked | no     | if =-Hi=                                    | =-Hi= only works for deterministic automata            |
-| =explicit-labels=   | checked | no     | always, unless =-Hi=                        |                                                        |
-| =state-acc=         | checked | yes    | re-checked, unless =-Ht= or =-Hm=           |                                                        |
-| =trans-acc=         | checked | no     | if not =state-acc= and not =-Hm=            |                                                        |
-| =no-univ-branch=    | ignored | no     | only if =-Hv=                               |                                                        |
-| =deterministic=     | checked | yes    | re-checked                                  |                                                        |
-| =complete=          | checked | no     | re-checked                                  |                                                        |
-| =unambiguous=       | trusted | yes    | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous=           |
-| =stutter-invariant= | trusted | yes    | as stored                                   | can be re-checked with =--check=stuttering=            |
-| =stutter-sensitive= | trusted | yes    | as stored                                   | can be re-checked with =--check=stuttering=            |
-| =terminal=          | trusted | yes    | as stored                                   | can be re-checked with =--check=strength=              |
-| =weak=              | trusted | yes    | as stored if (=-Hv= or not =terminal=)      | can be re-checked with =--check=strength=              |
-| =inherently-weak=   | trusted | yes    | as stored if (=-Hv= or not =weak=)          |                                                        |
-| =colored=           | ignored | no     | checked                                     |                                                        |
+| property            | parser  | stored | printer                                     | notes                                                            |
+|---------------------+---------+--------+---------------------------------------------+------------------------------------------------------------------|
+| =state-labels=      | checked | no     | re-rechecked if =-Hk=                       | state labels are converted to transition labels when reading TωA |
+| =trans-labels=      | checked | no     | always, unless =-Hi= or =-Hk=               |                                                                  |
+| =implicit-labels=   | checked | no     | if =-Hi=                                    | =-Hi= only works for deterministic automata                      |
+| =explicit-labels=   | checked | no     | always, unless =-Hi=                        |                                                                  |
+| =state-acc=         | checked | yes    | re-checked, unless =-Ht= or =-Hm=           |                                                                  |
+| =trans-acc=         | checked | no     | if not =state-acc= and not =-Hm=            |                                                                  |
+| =no-univ-branch=    | ignored | no     | only if =-Hv=                               |                                                                  |
+| =deterministic=     | checked | yes    | re-checked                                  |                                                                  |
+| =complete=          | checked | no     | re-checked                                  |                                                                  |
+| =unambiguous=       | trusted | yes    | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous=                     |
+| =stutter-invariant= | trusted | yes    | as stored                                   | can be re-checked with =--check=stuttering=                      |
+| =stutter-sensitive= | trusted | yes    | as stored                                   | can be re-checked with =--check=stuttering=                      |
+| =terminal=          | trusted | yes    | as stored                                   | can be re-checked with =--check=strength=                        |
+| =weak=              | trusted | yes    | as stored if (=-Hv= or not =terminal=)      | can be re-checked with =--check=strength=                        |
+| =inherently-weak=   | trusted | yes    | as stored if (=-Hv= or not =weak=)          |                                                                  |
+| =colored=           | ignored | no     | checked                                     |                                                                  |
 
 ** Named properties
 
diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc
index 811412e02..b236a711e 100644
--- a/src/bin/common_aoutput.cc
+++ b/src/bin/common_aoutput.cc
@@ -104,6 +104,7 @@ static const argp_option options[] =
       "(s) prefer state-based acceptance when possible [default], "
       "(t) force transition-based acceptance, "
       "(m) mix state and transition-based acceptance, "
+      "(k) use state labels when possible, "
       "(l) single-line output, "
       "(v) verbose properties", 0 },
     { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
diff --git a/src/tests/readsave.test b/src/tests/readsave.test
index aa271dbd3..08cf14dbf 100755
--- a/src/tests/readsave.test
+++ b/src/tests/readsave.test
@@ -633,7 +633,27 @@ EOF
 
 diff output2 expect2
 
+$autfilt -Hk expect2 >output2b
 
+cat >expect2b <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "p0" "p1"
+acc-name: all
+Acceptance: 0 t
+properties: state-labels explicit-labels state-acc deterministic
+--BODY--
+State: [!0&!1] 0
+1
+State: [0&1] 1
+2
+State: [!0&!1] 2
+0
+--END--
+EOF
+
+diff output2b expect2b
 
 # Check the difference between --remove-unreach and --remove-dead
 cat >input <<EOF
@@ -700,8 +720,8 @@ EOF
 diff output3 expect3
 
 
-$autfilt -Hk input 2>stderr && exit 1
-grep 'print_hoa.*k' stderr
+$autfilt -Hz input 2>stderr && exit 1
+grep 'print_hoa.*z' stderr
 
 cat >input4 <<EOF
 HOA: v1
@@ -773,3 +793,47 @@ State: 2 {0}
 --END--
 EOF
 diff output5 expect5
+
+cat >input6 <<EOF
+HOA: v1
+States: 3
+Start: 1
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: no-univ-branch trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[1] 2
+[1] 1
+[1] 1
+State: 1
+[0] 0
+[0] 1
+State: 2 {0}
+[0] 2
+[0] 0
+[0] 1
+--END--
+EOF
+
+run 0 $autfilt -Hk input6 >output6
+cat >expect6 <<EOF
+HOA: v1
+States: 3
+Start: 1
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: state-labels explicit-labels state-acc
+--BODY--
+State: [1] 0
+2 1 1
+State: [0] 1
+0 1
+State: [0] 2 {0}
+2 0 1
+--END--
+EOF
+
+diff output6 expect6
diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc
index 24968733f..f5340dde8 100644
--- a/src/twaalgos/hoa.cc
+++ b/src/twaalgos/hoa.cc
@@ -52,6 +52,7 @@ namespace spot
       bool is_deterministic;
       bool is_colored;
       bool use_implicit_labels;
+      bool use_state_labels = true;
       bdd all_ap;
 
       // Label support: the set of all conditions occurring in the
@@ -59,10 +60,12 @@ namespace spot
       typedef std::map<bdd, std::string, bdd_less_than> sup_map;
       sup_map sup;
 
-      metadata(const const_twa_graph_ptr& aut, bool implicit)
+      metadata(const const_twa_graph_ptr& aut, bool implicit,
+	       bool state_labels)
       {
 	check_det_and_comp(aut);
 	use_implicit_labels = implicit && is_deterministic && is_complete;
+	use_state_labels &= state_labels;
 	number_all_ap();
       }
 
@@ -106,8 +109,13 @@ namespace spot
 	    bool notfirst = false;
 	    acc_cond::mark_t prev = 0U;
 	    bool has_succ = false;
+	    bdd lastcond = bddfalse;
 	    for (auto& t: aut->out(src))
 	      {
+		if (has_succ)
+		  use_state_labels &= lastcond == t.cond;
+		else
+		  lastcond = t.cond;
 		if (complete)
 		  sum |= t.cond;
 		if (deterministic)
@@ -244,6 +252,7 @@ namespace spot
     hoa_acceptance acceptance = Hoa_Acceptance_States;
     bool implicit_labels = false;
     bool verbose = false;
+    bool state_labels = false;
 
     if (opt)
       while (*opt)
@@ -253,6 +262,9 @@ namespace spot
 	    case 'i':
 	      implicit_labels = true;
 	      break;
+	    case 'k':
+	      state_labels = true;
+	      break;
 	    case 'l':
 	      newline = false;
 	      break;
@@ -278,7 +290,7 @@ namespace spot
     // automata, so it has to be done first.
     unsigned init = aut->get_init_state_number();
 
-    metadata md(aut, implicit_labels);
+    metadata md(aut, implicit_labels, state_labels);
 
     if (acceptance == Hoa_Acceptance_States && !md.has_state_acc)
       acceptance = Hoa_Acceptance_Transitions;
@@ -399,8 +411,11 @@ namespace spot
     if (verbose)
       prop(" no-univ-branch");
     implicit_labels = md.use_implicit_labels;
+    state_labels = md.use_state_labels;
     if (implicit_labels)
       prop(" implicit-labels");
+    else if (state_labels)
+      prop(" state-labels explicit-labels");
     else
       prop(" trans-labels explicit-labels");
     if (acceptance == Hoa_Acceptance_States)
@@ -453,7 +468,20 @@ namespace spot
 	  this_acc = (md.common_acc[i] ?
 		      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
 
-	os << "State: " << i;
+	os << "State: ";
+	if (state_labels)
+	  {
+	    bool output = false;
+	    for (auto& t: aut->out(i))
+	      {
+		os << '[' << md.sup[t.cond] << "] ";
+		output = true;
+		break;
+	      }
+	    if (!output)
+	      os << "[f] ";
+	  }
+	os << i;
 	if (sn && i < sn->size() && !(*sn)[i].empty())
 	  os << " \"" << (*sn)[i] << '"';
 	if (this_acc == Hoa_Acceptance_States)
@@ -468,8 +496,9 @@ namespace spot
 	  }
 	os << nl;
 
-	if (!implicit_labels)
+	if (!implicit_labels && !state_labels)
 	  {
+
 	    for (auto& t: aut->out(i))
 	      {
 		os << '[' << md.sup[t.cond] << "] " << t.dst;
@@ -478,6 +507,24 @@ namespace spot
 		os << nl;
 	      }
 	  }
+	else if (state_labels)
+	  {
+	    unsigned n = 0;
+	    for (auto& t: aut->out(i))
+	      {
+		os << t.dst;
+		if (this_acc == Hoa_Acceptance_Transitions)
+		  {
+		    md.emit_acc(os, aut, t.acc);
+		    os << nl;
+		  }
+		else
+		  {
+		    ++n;
+		    os << (((n & 15) && t.next_succ) ? ' ' : nl);
+		  }
+	      }
+	  }
 	else
 	  {
 	    for (auto& t: aut->out(i))
diff --git a/src/twaalgos/hoa.hh b/src/twaalgos/hoa.hh
index 64d83ec6b..1f32d2b2f 100644
--- a/src/twaalgos/hoa.hh
+++ b/src/twaalgos/hoa.hh
@@ -32,7 +32,8 @@ namespace spot
   /// \param g The automaton to output.
   /// \param opt a set of characters each corresponding to a possible
   ///        option: (i) implicit labels for complete and
-  ///        deterministic automata, (s) state-based acceptance, (t)
+  ///        deterministic automata, (k) state labels when possible,
+  ///        (s) state-based acceptance when possible, (t)
   ///        transition-based acceptance, (m) mixed acceptance, (l)
   ///        single-line output, (v) verbose properties.
   SPOT_API std::ostream&