# Soundness and Completeness of a Model-Checking Proof System for CTL

Georg Friedrich Schuppe Dilian Gurov
KTH Royal Institute of Technology, Stockholm
<EMAIL_ADDRESS>
###### Abstract

We propose a local model-checking proof system for a fragment of CTL. The
rules of the proof system are motivated by the well-known fixed-point
characterisation of CTL based on unfolding of the temporal operators. To
guarantee termination of proofs, we tag the sequents of our proof system with
the set of states that have already been explored for the respective temporal
formula. We define the semantics of tagged sequents, and then state and prove
soundness and completeness of the proof system, as well as termination of
proof search for finite-state models.

##  1 Introduction

Computation Tree Logic (CTL) is a well-known branching-time temporal logic [3,
5]. Many useful temporal specification patterns can be expressed naturally in
CTL. The logic is supported by numerous off-the-shelf model checking tools
such as nuSMV [2].

The standard, _global_ approach to model checking of a CTL formula
$\textpm\phi$ w.r.t. a given state $s$ of a given Kripke structure
$\mathcal{M}$ is to first compute the set
$\llbracket\phi\rrbracket^{\mathcal{M}}$ of all states that satisfy the
formula, i.e., the _denotation_ of $\textpm\phi$, and then to check whether
$s\in\llbracket\phi\rrbracket^{\mathcal{M}}$. This approach allows the use of
_symbolic_ representations of the denotations of the formula and its
subformulas, typically as BDDs (as in nuSMV).

An alternative, _local_ approach is to start with the state $s$ and
incrementally explore its neighbourhood as required by the formula
$\textpm\phi$, by _unfolding_ the latter step-by-step. One obvious advantage
of this approach is that it only explores the part of the model that is
required to establish or reject the checked formula. Another advantage is that
local model checking can be phrased as proof search in a _deductive proof
system_. It can then be implemented in a straightforward manner in a logic
programming environment such as Prolog. This can be very useful for _education
purposes_ , since it gives the opportunity for students to create, without
much effort, an own tool that can analyse non-trivial models of system
behaviour (typically with up to a few thousand states). In fact, the model-
checking proof system presented here has been developed for and used in the
course _Logic for Computer Scientists_ , given at KTH Royal Institute of
Technology, Stockholm.

It is well-known that CTL can be embedded into the (alternation-free fragment
of the) modal $\mu$-calculus [6]. Since local model checking proof systems
have already been proposed for the latter logic, as for instance in [1],
designing one for CTL based on the embedding should be straightforward.
However, there are good reasons for designing a self-standing proof system,
like the one we propose here. The foremost reason for us has been to utilise
the circumstance that it is the alternation-free fragment of the modal
$\mu$-calculus that we need to take into account. This suggests that the
approach to guaranteeing termination of proof search employed in [6] of
_tagging_ formulas with the set of states that have already been explored
w.r.t. the formula (in this case essentially requiring only the outermost
fixed-point needs to be tagged) can be lifted from the level of formulas to
the level of sequents. Thus, tagged sequents need to be given a formal
semantics, to allow to state formally soundness and completeness of the proof
system, and to argue for termination of proof search for finite-state models.

Since our proof system has originally been designed for education purposes, to
keep the presentation simple, we have chosen not to include the Until operator
of CTL in our treatment, and leave its addition as an exercise to the
interested reader. This does not present any technical difficulties, and
simply follows the pattern of the other temporal operators and their fixed-
point characterisation.

##  2 Syntax and Semantics of the Logic

We start by presenting the syntax and semantics of the logic, which we call
$\mathrm{CTL^{-}}$, since it is a fragment of CTL.

######  Definition 2.1 (Logic Syntax).

The language is defined over a set of atomic propositions $\mathit{Atoms}$,
ranged over by $p$, as follows:

$\begin{array}[]{l}\phi\>::=\>p\>|\>\neg
p\>|\>\phi_{1}\wedge\phi_{2}\>|\>\phi_{1}\vee\phi_{2}\>|\>A\psi\>|\>E\psi\\\
\psi\>::=\>X\phi\>|\>G\phi\>|\>F\phi\end{array}$

The formulas $\phi$ are called _state formulas_ and $\psi$ _path formulas_.
The strict alternation of path and state quantifiers gives rise to six
combinations. Notice that negation is only allowed over atomic propositions.
The reason for this is that it is cumbersome to come up with a rule for
negated formulas in Section 3. However, this restriction does not affect the
expressiveness of the logic, since negated formulas can be “deMorganised” so
as to push the negation to the atomic propositions.

######  Definition 2.2 (Kripke Structure).

A _Kripke structure_ is a tuple $\mathcal{M}=(S,\xrightarrow[]{},L)$, where
$S$ is a set of _states_ , $\xrightarrow[]{}$ a binary _transition relation_
on $S$, and $L:S\rightarrow 2^{\mathit{Atoms}}$ a _labelling function_ that
assigns to every state the set of atomic propositions that are deemed true in
that state.

Given a Kripke structure, the semantics of a CTL formula $\phi$ is defined as
the set $\llbracket\phi\rrbracket^{\mathcal{M}}\subseteq S$ of states that
satisfy the formula, sometimes referred to as its _denotation_. Inspired by
[1], however, we shall define this notion relative to a set $U\subseteq S$ of
states, called a _tag_. We will use such tags in Section 3 to guarantee
finiteness of proof trees. Only formulas starting with a temporal operator
will need (non-empty) tags.

######  Definition 2.3 (Logic Semantics).

Let $\mathcal{M}=(S,\xrightarrow[]{},L)$ be a Kripke structure. The semantics
of formulas is inductively defined by the following equations:

$\displaystyle\llbracket p\rrbracket^{\mathcal{M}}_{\varnothing}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\\{s\in
S\;|\;p\in L(s)\\}$ (1) $\displaystyle\llbracket\neg
p\rrbracket^{\mathcal{M}}_{\varnothing}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad
S\setminus\llbracket p\rrbracket^{\mathcal{M}}_{\varnothing}$ (2)
$\displaystyle\llbracket\phi\wedge\psi\rrbracket^{\mathcal{M}}_{\varnothing}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\llbracket\phi\rrbracket^{\mathcal{M}}_{\varnothing}\cap\llbracket\psi\rrbracket^{\mathcal{M}}_{\varnothing}$
(3)
$\displaystyle\llbracket\phi\vee\psi\rrbracket^{\mathcal{M}}_{\varnothing}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\llbracket\phi\rrbracket^{\mathcal{M}}_{\varnothing}\cup\llbracket\psi\rrbracket^{\mathcal{M}}_{\varnothing}$
(4) $\displaystyle\llbracket
EX\phi\rrbracket^{\mathcal{M}}_{\varnothing}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\mathit{pre}_{\exists}(\llbracket\phi\rrbracket^{\mathcal{M}}_{\varnothing})$
(5) $\displaystyle\llbracket
AX\phi\rrbracket^{\mathcal{M}}_{\varnothing}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\mathit{pre}_{\forall}(\llbracket\phi\rrbracket^{\mathcal{M}}_{\varnothing})$
(6) $\displaystyle\llbracket EF\phi\rrbracket^{\mathcal{M}}_{U}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\mu
Y.(\llbracket\phi\rrbracket^{\mathcal{M}}_{\varnothing}\cup\mathit{pre}_{\exists}(Y)\setminus
U)$ (7) $\displaystyle\llbracket AF\phi\rrbracket^{\mathcal{M}}_{U}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\mu
Y.(\llbracket\phi\rrbracket^{\mathcal{M}}_{\varnothing}\cup\mathit{pre}_{\forall}(Y)\setminus
U)$ (8) $\displaystyle\llbracket EG\phi\rrbracket^{\mathcal{M}}_{U}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\nu
Y.(\llbracket\phi\rrbracket^{\mathcal{M}}_{\varnothing}\cap\mathit{pre}_{\exists}(Y)\cup
U)$ (9) $\displaystyle\llbracket AG\phi\rrbracket^{\mathcal{M}}_{U}\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\nu
Y.(\llbracket\phi\rrbracket^{\mathcal{M}}_{\varnothing}\cap\mathit{pre}_{\forall}(Y)\cup
U)$ (10)

where the state transformers $\mathit{pre}_{\exists}:S\xrightarrow[]{}S$ and
$\mathit{pre}_{\forall}:S\xrightarrow[]{}S$, and the _least_ and _greatest
fixed-point_ $\mu Y.f(Y)$ and $\nu Y.f(Y)$ of a monotone function
$f:S\xrightarrow[]{}S$ are defined as follows:

$\displaystyle\mathit{pre}_{\exists}(Y)\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\\{s\in
S\;|\;\exists s^{\prime}\in Y.\ s\xrightarrow[]{}s^{\prime}\\}$ (11)
$\displaystyle\mathit{pre}_{\forall}(Y)\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\\{s\in
S\;|\;\forall s^{\prime}\in S.\ (s\xrightarrow[]{}s^{\prime}\Rightarrow
s^{\prime}\in Y)\\}$ (12) $\displaystyle\mu Y.f(Y)\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\bigcap\
\\{X\subseteq S\;|\;f(X)\subseteq X\\}$ (13) $\displaystyle\nu Y.f(Y)\quad$
$\displaystyle\stackrel{{\scriptstyle\mathclap{\mbox{def}}}}{{=}}\quad\bigcup\
\\{X\subseteq S\;|\;f(X)\supseteq X\\}$ (14)

If the tag $U$ is empty, the semantics coincides with the standard semantics
of CTL. The semantic rules for $\llbracket
EF\phi\rrbracket^{\mathcal{M}}_{\varnothing}$, $\llbracket
AF\phi\rrbracket^{\mathcal{M}}_{\varnothing}$, $\llbracket
EG\phi\rrbracket^{\mathcal{M}}_{\varnothing}$ and $\llbracket
AG\phi\rrbracket^{\mathcal{M}}_{\varnothing}$ fall back on known embeddings of
CTL into the modal $\mu$-calculus [4].

We shall later need the following result.

######  Lemma 2.1 (Reduction Lemma [1]).

For any monotone function $\psi$ on a powerset $\mathit{Pow}(D)$, and any
$p\in D$, we have:

$\displaystyle p\in\mu Y.\psi(Y)$
$\displaystyle\>\Leftrightarrow\>p\in\psi(\mu Y.(\psi(Y)\setminus\\{p\\}))$
(15) $\displaystyle p\in\nu Y.\psi(Y)$
$\displaystyle\>\Leftrightarrow\>p\in\psi(\nu Y.(\psi(Y)\cup\\{p\\}))$ (16)

The right-hand sides of these logical equivalences involve a slightly modified
unfolding of the fixed points: For the least fixed point of a single element,
$p$ is removed in the unfolding; for the greatest it is added.

##  3 A Local Model-Checking Proof System

${p}\>\>\frac{-}{\mathcal{M},s\>\vdash_{\varnothing}\>p}\>\>{p\in L(s)}\hskip
42.67912pt{\neg p}\>\>\frac{-}{\mathcal{M},s\>\vdash_{\varnothing}\>\neg
p}\>\>{p\not\in L(s)}$
${\wedge}\>\>\frac{\mathcal{M},s\>\vdash_{\varnothing}\>\phi\hskip
28.45274pt\mathcal{M},s\>\vdash_{\varnothing}\>\psi}{\mathcal{M},s\>\vdash_{\varnothing}\>\phi\wedge\psi}\>\>{}$
${\vee_{1}}\>\>\frac{\mathcal{M},s\>\vdash_{\varnothing}\>\phi}{\mathcal{M},s\>\vdash_{\varnothing}\>\phi\vee\psi}\>\>{}\hskip
42.67912pt{\vee_{2}}\>\>\frac{\mathcal{M},s\>\vdash_{\varnothing}\>\psi}{\mathcal{M},s\>\vdash_{\varnothing}\>\phi\vee\psi}\>\>{}$
${\mbox{\sf AX}}\>\>\frac{\mathcal{M},s_{1}\>\vdash_{\varnothing}\>\phi\hskip
14.22636pt\cdots\hskip
14.22636pt\mathcal{M},s_{n}\>\vdash_{\varnothing}\>\phi}{\mathcal{M},s\>\vdash_{\varnothing}\>\mbox{\sf
AX}\ \phi}\>\>{}$ ${\mbox{\sf
AG}_{1}}\>\>\frac{-}{\mathcal{M},s\>\vdash_{U}\>\mbox{\sf AG}\ \phi}\>\>{s\in
U}\hskip 42.67912pt{\mbox{\sf
AF}_{1}}\>\>\frac{\mathcal{M},s\>\vdash_{\varnothing}\>\phi}{\mathcal{M},s\>\vdash_{U}\>\mbox{\sf
AF}\ \phi}\>\>{s\not\in U}$ ${\mbox{\sf
AG}_{2}}\>\>\frac{\mathcal{M},s\>\vdash_{\varnothing}\>\phi\hskip
28.45274pt\mathcal{M},s_{1}\>\vdash_{U,s}\>\mbox{\sf AG}\ \phi\hskip
5.69054pt\cdots\hskip 5.69054pt\mathcal{M},s_{n}\>\vdash_{U,s}\>\mbox{\sf AG}\
\phi}{\mathcal{M},s\>\vdash_{U}\>\mbox{\sf AG}\ \phi}\>\>{s\not\in U}$
${\mbox{\sf AF}_{2}}\>\>\frac{\mathcal{M},s_{1}\>\vdash_{U,s}\>\mbox{\sf AF}\
\phi\hskip 14.22636pt\cdots\hskip
14.22636pt\mathcal{M},s_{n}\>\vdash_{U,s}\>\mbox{\sf AF}\
\phi}{\mathcal{M},s\>\vdash_{U}\>\mbox{\sf AF}\ \phi}\>\>{s\not\in U}$
${\mbox{\sf
EX}}\>\>\frac{\mathcal{M},s^{\prime}\>\vdash_{\varnothing}\>\phi}{\mathcal{M},s\>\vdash_{\varnothing}\>\mbox{\sf
EX}\ \phi}\>\>{}\hskip 42.67912pt{\mbox{\sf
EG}_{1}}\>\>\frac{-}{\mathcal{M},s\>\vdash_{U}\>\mbox{\sf EG}\ \phi}\>\>{s\in
U}$ ${\mbox{\sf
EG}_{2}}\>\>\frac{\mathcal{M},s\>\vdash_{\varnothing}\>\phi\hskip
28.45274pt\mathcal{M},s^{\prime}\>\vdash_{U,s}\>\mbox{\sf EG}\
\phi}{\mathcal{M},s\>\vdash_{U}\>\mbox{\sf EG}\ \phi}\>\>{s\not\in U}$
${\mbox{\sf
EF}_{1}}\>\>\frac{\mathcal{M},s\>\vdash_{\varnothing}\>\phi}{\mathcal{M},s\>\vdash_{U}\>\mbox{\sf
EF}\ \phi}\>\>{s\not\in U}\hskip 42.67912pt{\mbox{\sf
EF}_{2}}\>\>\frac{\mathcal{M},s^{\prime}\>\vdash_{U,s}\>\mbox{\sf EF}\
\phi}{\mathcal{M},s\>\vdash_{U}\>\mbox{\sf EF}\ \phi}\>\>{s\not\in U}$

Figure 1: A Local Model-Checking Proof System for $\mathrm{CTL^{-}}$.

We present our model-checking procedure in the form of a deductive system,
consisting of rules over sequents $\mathcal{M},s\>\vdash_{U}\>\phi$. To
guarantee finiteness of proof trees, and with this completeness of the proof
systems as well as termination of proof search, we equip our sequents with
_tags_ $U\subseteq S$ as already introduced in Section 2. The rules of our
proof system are presented in Figure 1. In the premises of the A-rules,
$s_{1},\dots,s_{n}$ denote _all_ successors of state $s$ in the Kripke
structure $\mathcal{M}$, while in the premises of the E-rules, $s^{\prime}$
denotes _some_ successor of $s$. To prove that a state $s$ in a Kripke
structure $\mathcal{M}$ satisfies a formula $\phi$ of the logic, one needs to
derive the sequent $\mathcal{M},s\vdash_{\varnothing}\phi$, where the tag is
initially empty.

_Example._ Consider the following Kripke structure:

$p,q$$q,r$$r$$s_{0}$$s_{1}$$s_{2}$

We would like to show that the formula $\mbox{\sf EF}\ (\mbox{\sf EG}\ r)$
holds in state $s_{0}$ of the Kripke structure. This can be established by the
following proof tree:

$\mathcal{M},s_{0}\vdash_{\varnothing}\mbox{\sf EF}\ (\mbox{\sf EG}\
r)\mathcal{M},s_{2}\vdash_{[s_{0}]}\mbox{\sf EF}\ (\mbox{\sf EG}\
r)\mathcal{M},s_{2}\vdash_{\varnothing}\mbox{\sf EG}\
r\lx@proof@logical@and\mathcal{M},s_{2}\vdash_{\varnothing}r-\mathcal{M},s_{2}\vdash_{[s_{2}]}\mbox{\sf
EG}\ r-$

To define and prove the properties of the proof system we need the following
semantic notion.

######  Definition 3.1 (Sequent Validity).

A sequent $\mathcal{M},s\vdash_{U}\phi$ is termed _valid_ , denoted
$\mathcal{M},s\models_{U}\phi$, iff
$s\in\llbracket\phi\rrbracket^{\mathcal{M}}_{U}$.

##  4 Soundness of the Proof System

A deductive system is termed _sound_ if all sequents derivable with its rules
are semantically valid (that is, only valid sequents can be proved). We will
show that all rules of our proof system preserve the validity of sequents
whenever the respective side condition holds. For readability, we omit the
superscript $\mathcal{M}$, when it is clear which $\mathcal{M}$ is meant. We
abbreviate ${U\cup\\{s\\}}$ by writing $U,s$.

######  Theorem 4.1 (Soundness).

The proof system from Figure 1 is sound.

_Proof_. The result is a direct consequence of the soundness of each rule,
which we show here. Recall that a rule is termed sound if its conclusion is a
valid sequent whenever all its premises are valid and the side-conditions
hold.

_Rule $p$_. If $p\in L(s)$, the conclusion
$\mathcal{M},s\models_{\varnothing}p$ follows directly from Definition 3.1 and
(1). The argument for rule $\neg p$ is dual.

_Rule $\wedge$_. We show that $\mathcal{M},s\models_{\varnothing}\phi$ and
$\mathcal{M},s\models_{\varnothing}\psi$ imply
$\mathcal{M},s\models_{\varnothing}\phi\wedge\psi$. If
$s\in\llbracket\phi\rrbracket_{\varnothing}$ and
$s\in\llbracket\psi\rrbracket_{\varnothing}$, then obviously

$s\in\llbracket\phi\rrbracket_{\varnothing}\cap\llbracket\psi\rrbracket_{\varnothing}\stackrel{{\scriptstyle\eqref{eq:sem_and}}}{{=}}\llbracket\phi\wedge\psi\rrbracket_{\varnothing}.$

_Rules $\vee_{1},\vee_{2}$_. We show that
$\mathcal{M},s\models_{\varnothing}\phi$ implies
$\mathcal{M},s\models_{\varnothing}\phi\vee\psi$. If
$s\in\llbracket\phi\rrbracket_{\varnothing}$, then

$s\in\llbracket\phi\rrbracket_{\varnothing}\cup\llbracket\psi\rrbracket_{\varnothing}\stackrel{{\scriptstyle\eqref{eq:sem_or}}}{{=}}\llbracket\phi\vee\psi\rrbracket_{\varnothing}.$

The argument for $\vee_{2}$ is similar.

_Rule $EX$_. We show that $\mathcal{M},s^{\prime}\models_{\varnothing}\phi$
implies $\mathcal{M},s\models_{\varnothing}EX\phi$, where
$s\xrightarrow[]{}s^{\prime}$ with $s,s^{\prime}\in S$. If
$s^{\prime}\in\llbracket\phi\rrbracket_{\varnothing}$, then with (11), it
holds that

$s\in\mathit{pre}_{\exists}(\llbracket\phi\rrbracket_{\varnothing})\stackrel{{\scriptstyle\eqref{eq:sem_ex}}}{{=}}\llbracket
EX\phi\rrbracket_{\varnothing}.$

The reasoning for $AX$ and $\mathit{pre}_{\forall}$ is similar.

_Rule $EG_{1}$_. If $s\in U$, then $s\in\llbracket EG\phi\rrbracket_{U}$ holds
by (9).

_Rule $EG_{2}$_. We show that $\mathcal{M},s\models_{\varnothing}\phi$ and
$\mathcal{M},s^{\prime}\models_{U,s}EG\phi$ imply
$\mathcal{M},s\models_{U}EG\phi$ when $s\not\in U$, where
$s\xrightarrow[]{}s^{\prime}$ with $s,s^{\prime}\in S$. Applying the
appropriate semantic rule, and unfolding the fixed point once using Lemma 2.1,
we get the equivalences

$\displaystyle s\in\llbracket EG\phi\rrbracket_{U}$
$\displaystyle\stackrel{{\scriptstyle\eqref{eq:sem_eg}}}{{\Leftrightarrow}}\quad$
$\displaystyle s\in\nu
Y.(\llbracket\phi\rrbracket_{\varnothing}\cap\mathit{pre}_{\exists}(Y)\cup U)$
$\displaystyle\stackrel{{\scriptstyle\eqref{eq:nu_unf}}}{{\Leftrightarrow}}\quad$
$\displaystyle
s\in\llbracket\phi\rrbracket_{\varnothing}\cap\mathit{pre}_{\exists}(\nu
Y.(\llbracket\phi\rrbracket_{\varnothing}\cap\mathit{pre}_{\exists}(Y)\cup
U\cup\\{s\\}))\cup U$
$\displaystyle\stackrel{{\scriptstyle\eqref{eq:sem_eg}}}{{\Leftrightarrow}}\quad$
$\displaystyle
s\in\llbracket\phi\rrbracket_{\varnothing}\cap\mathit{pre}_{\exists}(\llbracket
EG\phi\rrbracket_{U,s})\cup U$

Since we assume $\mathcal{M},s^{\prime}\models_{U,s}EG\phi$, we have
$s^{\prime}\in\llbracket EG\phi\rrbracket_{U,s}$ and thus
$s\in\mathit{pre}_{\exists}(\llbracket EG\phi\rrbracket_{U,s})$. Together with
the assumption that $s\in\llbracket\phi\rrbracket_{\varnothing}$, we can
conclude that $s\in\llbracket EG\phi\rrbracket_{U}$, and hence
$\mathcal{M},s\models_{U}EG\phi$.

_Rule $EF_{1}$_. We show that $\mathcal{M},s\models_{\varnothing}\phi$ implies
$\mathcal{M},s\models_{U}EF\phi$ when $s\not\in U$. We have the equivalences

$\displaystyle s\in\llbracket EF\phi\rrbracket_{U}$
$\displaystyle\stackrel{{\scriptstyle\eqref{eq:sem_ef}}}{{\Leftrightarrow}}\quad$
$\displaystyle s\in\mu
Y.(\llbracket\phi\rrbracket_{\varnothing}\cup\mathit{pre}_{\exists}(Y)\setminus
U)$
$\displaystyle\stackrel{{\scriptstyle\eqref{eq:mu_unf}}}{{\Leftrightarrow}}\quad$
$\displaystyle
s\in\llbracket\phi\rrbracket_{\varnothing}\cup\mathit{pre}_{\exists}(\mu
Y.(\llbracket\phi\rrbracket_{\varnothing}\cup\mathit{pre}_{\exists}(Y)\setminus
U\setminus\\{s\\}))\setminus U$
$\displaystyle\stackrel{{\scriptstyle\eqref{eq:sem_ef}}}{{\Leftrightarrow}}\quad$
$\displaystyle
s\in\llbracket\phi\rrbracket_{\varnothing}\cup\mathit{pre}_{\exists}(\llbracket
EF\phi\rrbracket_{U,s})\setminus U$

Now, we can observe that

$s\in\llbracket\phi\rrbracket_{\varnothing}\cup\mathit{pre}_{\exists}(\llbracket
EF\phi\rrbracket_{U,s})\setminus U$

holds when $s\in\llbracket\phi\rrbracket_{\varnothing}$ and $s\not\in U$, and
hence $\mathcal{M},s\models_{U}EF\phi$.

_Rule $EF_{2}$_. We show that $\mathcal{M},s^{\prime}\models_{U,s}EF\phi$ and
$s\not\in U$ imply $\mathcal{M},s\models_{U}EF\phi$. Since we assume
$s^{\prime}\in\llbracket EF\phi\rrbracket_{U,s}$ and $s\not\in U$, by the same
equivalences as in the previous case we can conclude that $s\in\llbracket
EF\phi\rrbracket_{U}$, and hence $\mathcal{M},s\models_{U}EF\phi$.

_Rule $AG_{1}$_. If $s\in U$, then $s\in\llbracket AG\phi\rrbracket_{U}$ holds
by (10).

_Rule $AG_{2}$_. The argument is similar to the proof of $EG_{2}$.

_Rule $AF_{1}$_. The argument is similar to the proof of $EF_{1}$.

_Rule $AF_{2}$_. The argument is similar to the proof of $EF_{2}$.

This concludes the proof of soundness. $\hfill\blacksquare$

##  5 Completeness of the Proof System

A deductive system is termed _complete_ if for every semantically valid
sequent there exists a derivation of that sequent (that is, all valid sequents
can be proved). We show completeness by using the idea of a _canonical proof_.
The idea of the proof is that for every valid sequent there is a way to apply
rules backwards that is guaranteed to terminate with axiom rules as leaves,
and thus, produce a proof of the sequent.

###  5.1 Reversibility

First, we show that all rules are _reversible_ : For each rule, if the
conclusion is valid, then there exists a rule that can be applied backward, so
that the premises are valid.

######  Theorem 5.1 (Reversibility).

The rules of the proof system from Figure 1 are reversible.

_Proof_. We consider each rule in turn.

_Rule $\wedge$_. If $\mathcal{M},s\models_{\varnothing}\phi\wedge\psi$ is
valid, we can apply Rule $\wedge$ backwards. If
$s\in\llbracket\phi\wedge\psi\rrbracket_{\varnothing}$, then necessarily
$s\in\llbracket\phi\rrbracket_{\varnothing}$ and
$s\in\llbracket\phi\rrbracket_{\varnothing}$, and thus all premises of Rule
$\wedge$ are valid, enabling backward application of the rule.

_Rules $\vee_{1},\vee_{2}$_. If
$\mathcal{M},s\models_{\varnothing}\phi\vee\psi$ is valid, then
$s\in\llbracket\phi\vee\psi\rrbracket_{\varnothing}$, and hence necessarily
either $s\in\llbracket\phi\rrbracket_{\varnothing}$ or
$s\in\llbracket\phi\rrbracket_{\varnothing}$ has to hold. Thus, either the
premises of Rule $\vee_{1}$ or those of $\vee_{2}$ are valid and the
corresponding rule can be applied backwards.

_Rules $EX,AX$_. Assuming $\mathcal{M},s\models_{\varnothing}EX\phi$ is valid,
then $s\in\mathit{pre}_{\exists}(\llbracket\phi\rrbracket_{\varnothing})$ by
(5). Using the definition of $\mathit{pre}_{\exists}$ (11), we can conclude
that existence of a $s^{\prime}\in S$ with $s\xrightarrow[]{}s^{\prime}$ and
$s^{\prime}\in\llbracket\phi\rrbracket_{\varnothing}$ is necessary and thus
$\mathcal{M},s^{\prime}\models_{\varnothing}\phi$ is valid. The reasoning for
rule $AX$ and $\mathit{pre}_{\forall}$ is similar.

_Rule $EG_{1}$_. Assuming $\mathcal{M},s\models_{U}EG\phi$ and $s\in U$, there
is no premise to be proven valid and the rule is always applicable backwards.

_Rule $EG_{2}$_. If we assume $\mathcal{M},s\models_{U}EG\phi$, but $s\not\in
U$, we have to show that $\mathcal{M},s\models_{\varnothing}\phi$ and
$\mathcal{M},s^{\prime}\models_{U,s}EG\phi$. Unfolding the fixed point using
Lemma 2.1, we get

$s\in\llbracket EG\phi\rrbracket_{U}\Leftrightarrow
s\in\llbracket\phi\rrbracket_{\varnothing}\cap\mathit{pre}_{\exists}(\llbracket
EG\phi\rrbracket_{U,s})\cup U.$

Since $s\not\in U$, then necessarily
$s\in\llbracket\phi\rrbracket_{\varnothing}$ and
$s\in\mathit{pre}_{\exists}(\llbracket EG\phi\rrbracket_{U,s})$. From
$s\in\mathit{pre}_{\exists}(\llbracket EG\phi\rrbracket_{U,s})$, we can
conclude that there exists a $s^{\prime}$ with $s\xrightarrow[]{}s^{\prime}$
and $\mathcal{M},s^{\prime}\models_{U,s}EG\phi$.
$\mathcal{M},s\models_{\varnothing}\phi$ follows directly.

_Rules $EF_{1},EF_{2}$_. Assuming $\mathcal{M},s\models_{U}EF\phi$ and
$s\not\in U$, we can obtain

$s\in\llbracket EF\phi\rrbracket_{U}\Leftrightarrow
s\in\llbracket\phi\rrbracket_{\varnothing}\cup\mathit{pre}_{\exists}(\llbracket
EF\phi\rrbracket_{U,s})\setminus U$

through unfolding of the fixed point once using Lemma 2.1. Since $s\not\in U$,
either $s\in\llbracket\phi\rrbracket_{\varnothing}$ or
$s\in\mathit{pre}_{\exists}(\llbracket EF\phi\rrbracket_{U,s})$ is necessarily
valid. From $s\in\llbracket\phi\rrbracket_{\varnothing}$ follows
$\mathcal{M},s\models_{\varnothing}\phi$. From
$s\in\mathit{pre}_{\exists}(\llbracket EF\phi\rrbracket_{U,s})$, we can
conclude that there exists a $s^{\prime}$ with $s\xrightarrow[]{}s^{\prime}$
and $\mathcal{M},s^{\prime}\models_{U,s}EF\phi$. Thus, either $EF_{1}$ or
$EF_{2}$ is always applicable backwards when the conclusion is valid.

_Rules $AG_{1},AG_{2}$_. The argument is similar to the reversibly of
_$EG_{1}$_ and _$EG_{2}$_.

_Rules $AF_{1},AF_{2}$_. The argument is similar to the reversibility of
_$EF_{1}$_ and _$EF_{2}$_.

This concludes the proof of reversibility. $\hfill\blacksquare$

Hence, starting a proof from any semantically valid sequent, there is a way to
“grow” a derivation tree upwards, maintaining semantic validity as an
invariant property of the nodes of the derivation tree.

###  5.2 Termination

To obtain a (canonical) proof, however, we need to argue that every branch of
the tree is bound to terminate, and furthermore with an axiom.

######  Lemma 5.1 (Finiteness of Derivation Trees).

Every derivation produced with the rules of the proof system from Figure 1 is
finite for finite-state Kripke structures.

_Proof_. Between conclusion and premises, we observe that application of each
reversible rule either $(i)$ decreases the length of the sequent formulas or
$(ii)$ decreases the number of leftover untagged states $S\setminus U$.
Defining a lexicographical ordering through these two criteria on a series of
backward applications, it is easy to see that such a series would be
monotonically decreasing. $\hfill\blacksquare$

###  5.3 Completeness

Finally, we are ready to show completeness of our proof system.

######  Theorem 5.2 (Completeness).

The proof system from Figure 1 is complete for finite-state Kripke structures.

_Proof_. For any valid sequent, by Theorem 5.1, there always exists a
backwards applicable rule, and, by Lemma 5.1, any series of backward rule
applications is terminating. Thus, eventually, every branch must terminate by
reverse application of an axiom rule, and hence, there exists a proof of the
sequent. $\hfill\blacksquare$

Observe that soundness, completeness, and finiteness of derivation trees
guarantee _decidability_ of sequent validity.

##  6 Conclusion

In this paper, we have presented a local model-checking proof system for a
fragment of CTL, and have proved its soundness and completeness, and
termination of proof search for finite-state models. Extending the proof
system and the proofs to the full CTL is a routine exercise.

The proof system has been developed for and used in the course _Logic for
Computer Scientists_ , given at KTH Royal Institute of Technology, Stockholm.

## References

  * [1] Henrik Reif Andersen, Colin Stirling, and Glynn Winskel.  A compositional proof system for the modal mu-calculus.  In Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pages 144–153. IEEE, 1994.
  * [2] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella.  NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking.  In Proc. International Conference on Computer-Aided Verification (CAV 2002), volume 2404 of LNCS, Copenhagen, Denmark, July 2002. Springer.
  * [3] Edmund M. Clarke and E. Allen Emerson.  Design and synthesis of synchronization skeletons using branching-time temporal logic.  In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer, 1981.
  * [4] Stéphane Demri, Valentin Goranko, and Martin Lange.  Branching-Time Temporal Logics.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.
  * [5] Michael Huth and Mark Dermot Ryan.  Logic in computer science - modelling and reasoning about systems (2. ed.).  Cambridge University Press, 2004.
  * [6] Dexter Kozen.  Results on the propositional $\mathrm{\mu}$-calculus.  In Mogens Nielsen and Erik Meineche Schmidt, editors, Automata, Languages and Programming, 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings, volume 140 of Lecture Notes in Computer Science, pages 348–359. Springer, 1982.


# Subgroups with a small sum of element orders

Mihai-Silviu Lazorec

(August 2, 2022)

###### Abstract

A finite group $G$ is said to be a $\mathscr{B}_{\psi}$-group if $\psi(H)<|G|$
for any proper subgroup $H$ of $G$, where $\psi(H)$ denotes the sum of element
orders of $H$. In this paper, we characterize the $\mathscr{B}_{\psi}$-groups
up to the class of finite nilpotent groups. We also study the above inequality
in the case of finite $P$-groups and Schmidt groups, respectively.

MSC (2020): Primary 20D60; Secondary 20D10, 20D15, 20D25, 20E28.

Key words: group element orders, nilpotent groups, $P$-groups, Schmidt groups.

##  1 Introduction

Let $G$ be a finite group and let $n$ be a positive integer. We denote by
$o(x),exp(G),\pi(G)$ and $C_{n}$ the order of an element $x\in G$, the
exponent of $G$, the set of prime divisors of $|G|$ and the cyclic group of
order $n$, respectively. By adding all element orders of $G$, we get the
quantity

$\psi(G)=\sum\limits_{x\in G}o(x)$

known as the sum of element orders of $G$. During the past 12 years, this
quantity was of some interest especially because it was proved that it can be
used to characterize various classes of finite groups. More exactly, for a
group $G$ of order $n$, it was shown that if
$\frac{\psi(G)}{\psi(C_{n})}>\alpha$, for some $\alpha\in(0,1)$, then $G$ is
cyclic/nilpotent/supersolvable/solvable (see [3, 5, 6, 12, 17]). For each
case, the best lower bound $\alpha$ was precisely determined as being
$\alpha=\frac{\psi(H)}{\psi(C_{|H|})}$, where $H$ is the smallest non-
cyclic/non-nilpotent/non-supersolvable/non-solvable group.

In [1], it was proved that the maximum value of the sum of element orders
among all groups of order $n$ is $\psi(C_{n})$. This means that if $G$ is a
group of order $n$, then $\psi(G)\leq\psi(C_{n})$ and the equality holds if
and only if $G\cong C_{n}$. Obviously one may ask if something can be said
about the minimum value of the sum of element orders. An answer is given up to
nilpotent groups. More exactly, in [2], the authors proved the following
result:

Theorem 1.1. Let $G$ be a group of order $n$. Then $\psi(G)\leq\psi(H)$ for
every nilpotent group $H$ of order $n$ if and only if the Sylow subgroups of
$G$ are of prime exponent.

In [11], the authors classified the finite abelian groups determined by an
inequality involving the sum of element orders. They said that a finite group
$G$ is a $\mathscr{B}_{\psi}$-group if the inequality

$\psi(H)<|G|$

holds for all proper subgroups $H$ of $G$. Obviously, in order to inspect if
$G$ is a $\mathscr{B}_{\psi}$-group, it suffices to check if the maximal
subgroups of $G$ satisfy the above mentioned inequality. The classification of
the finite abelian $\mathscr{B}_{\psi}$-groups is the following one:

Theorem 1.2. Let $G$ be a finite abelian group. Then $G$ is a
$\mathscr{B}_{\psi}$-group if and only if $G\cong C_{p^{2}}$ or $G\cong
C_{p}^{n}$, where $p$ is a prime and $n\geq 1$.

Intuitively, both theorems conclude that if one wants to lower the sum of
element orders of a finite group $G$, then a significant part of the group
element orders should be equal to a prime/square-free number/square of a
prime. The results of this paper also support this idea. Our main objective is
to study the $\mathscr{B}_{\psi}$ property beyond finite abelian groups. A
first step is to outline a connection between this property and a specific
normal Hall $\pi$-subgroup of a finite group $G$. Then, we show that a finite
nilpotent group $G$ is a $\mathscr{B}_{\psi}$-group if and only if $G\cong
C_{p^{2}}$ or $G$ is a $p$-group with $exp(G)=p$. We enumerate the non-
nilpotent solvable $\mathscr{B}_{\psi}$-groups up to order 2000. Such a group
$G$ has the property $|\pi(G)|=2$. Inspired by this remark, we study the
$\mathscr{B}_{\psi}$ property of two classes of finite groups whose orders are
divisible by two primes: $P$-groups and Schmidt groups.

We recall the definition of a finite $P$-group by following section 2.2 of
[15]. Let $p$ be a prime number and $n\geq 2$ be an integer. We say that a
finite group $G$ belongs to the class $P(n,p)$ if $G$ is either an elementary
abelian $p$-group of order $p^{n}$, or a semidirect product of an elementary
abelian normal $p$-subgroup $H$ of order $p^{n-1}$ by a group of prime order
$q\neq p$ which induces a non-trivial power automorphism on $H$. We call $G$ a
$P$-group if $G$ belongs to $P(n,p)$, for some prime $p$ and some integer
$n\geq 2$. If $p=2$, it is known that the elementary abelian 2-groups are the
only finite $P$-groups, while if $p>2$, besides the elementary abelian
$p$-group, one can construct a non-abelian $P$-group containing elements of
order $q$, for every prime $q$ such that $q|(p-1)$.

We end this section by pointing out that some further research directions are
outlined throughout the paper.

##  2 Main results

We begin this section by recalling some well-known results concerning the
multiplicativity property of $\psi$ and the computation of the sum of element
orders of a finite cyclic $p$-group. Also, we prove an inequality that is
going to be used at some point.

Lemma 2.1. The following statements hold:

  * i)

$\psi(C_{p^{n}})=\frac{p^{2n+1}+1}{p+1}$, where $p$ is prime and $n\geq 1$ is
an integer;

  * ii)

Let $G_{1}$ and $G_{2}$ be finite groups. Then $\psi(G_{1}\times
G_{2})\leq\psi(G_{1})\psi(G_{2})$ and the equality holds if and only if
$(|G_{1}|,|G_{2}|)=1$;

  * iii)

Let $p,q$ be distinct primes and let $\alpha\geq 1,\beta\geq 2$ be some
integers. Then
$\psi(C_{p}^{\alpha})\psi(C_{q}^{\beta-1})>p^{\alpha}q^{\beta}.$

Proof. For the first two items, the reader may check Lemma 2.1 of [2] and
Lemma 2.9 (1) of [12], respectively. For iii), we have

$\psi(C_{p}^{\alpha})\psi(C_{q}^{\beta-1})>p^{\alpha}q^{\beta}\Longleftrightarrow(p^{\alpha+1}-p+1)(q^{\beta}-q+1)-p^{\alpha}q^{\beta}>0.$

To prove the above inequality, it suffices to show that the function
$f:[2,\infty)\longrightarrow\mathbb{R}$, given by

$f(x)=(px-p+1)(q^{\beta}-q+1)-xq^{\beta},\ \forall\ x\in[2,\infty),$

takes positive values. Obviously, $f$ is derivable and

$f^{\prime}(x)=(p-1)q^{\beta}-pq+p\geq(p-1)q^{2}-pq+p>0,$

so $f(x)\geq f(2),\ \forall\ x\in[2,\infty)$. Since

$f(2)=(p+1)(q^{\beta}-q+1)-2q^{\beta}\geq q^{\beta}-3q+3\geq q^{2}-3q+3>0,$

it follows that $f$ takes only positive values. Hence, the proof is complete.

Since a finite nilpotent group is isomorphic to the direct product of its
Sylow subgroups, to investigate the $\mathscr{B}_{\psi}$ property of such a
group, we need to solve the case of finite $p$-groups first.

Proposition 2.2. Let $G$ be a finite $p$-group. Then $G$ is a
$\mathscr{B}_{\psi}$-group if and only if $G\cong C_{p^{2}}$ or $exp(G)=p$.

Proof. Let $G$ be a $p$-group of order $p^{n}$, where $n\geq 1$. Assume that
$G$ is a $\mathscr{B}_{\psi}$-group. If $n\in\\{1,2\\}$, then $G\cong
C_{p^{2}}$ or $exp(G)=p$, as desired. Let $n\geq 3$ and $exp(G)=p^{m}$, where
$m\geq 1$. Clearly $m<n$ since otherwise $G$ would be a cyclic
$\mathscr{B}_{\psi}$-group of order $|G|\geq p^{3}$. Then the conclusion of
Theorem 1.2 would not hold, a contradiction. It follows that there is a
maximal subgroup $H$ of $G$ containing an element of order $p^{m}$. We get

$\psi(H)\geq 1+p^{m}+(p^{n-1}-2)p=|G|+p^{m}-2p+1.$

If $m\geq 2$, we obtain $\psi(H)\geq|G|+(p-1)^{2}>|G|$, contradicting the
$\mathscr{B}_{\psi}$ property of $G$. Hence, $m=1$ and $exp(G)=p$.

Conversely, if $G\cong C_{p^{2}}$, then $G$ is a $\mathscr{B}_{\psi}$-group by
Theorem 1.2. If $exp(G)=p$, then for any maximal subgroup $H$ of $G$ we have

$\psi(H)=1+(p^{n-1}-1)p=|G|-p+1<|G|,$

so once again $G$ is a $\mathscr{B}_{\psi}$-group.

In general, the direct product of two $\mathscr{B}_{\psi}$-groups is not a
$\mathscr{B}_{\psi}$-group. For instance, according to Theorem 1.2 we know
that $C_{2}$ and $C_{3}$ are $\mathscr{B}_{\psi}$-groups, while $C_{6}$ is
not. Also, in general the $\mathscr{B}_{\psi}$ property of a finite group is
not inherited by its non-trivial subgroups. The smallest example in this
regard is $A_{5}$. Its maximal subgroups are isomorphic to $D_{10},S_{3}$ or
$A_{4}$. We have $\psi(D_{10})=\psi(A_{4})=31$ and $\psi(S_{3})=13$. All these
sums of element orders are less than $|A_{5}|=60$, so $A_{5}$ is a
$\mathscr{B}_{\psi}$-group. However, $\psi(C_{5})=21>10=|D_{10}|$, so $D_{10}$
is not a $\mathscr{B}_{\psi}$-group. In what concerns the inheritance of the
$\mathscr{B}_{\psi}$ property by non-trivial subgroups, we can use Proposition
2.2 to say more in the case of finite $p$-groups.

Corollary 2.3. Let $G$ be a finite $p$-group. Then all non-trivial subgroups
of $G$ are $\mathscr{B}_{\psi}$-groups if and only if $G\cong C_{p^{2}}$ or
$exp(G)=p$.

Proof. Let $G$ be a finite $p$-group. If all non-trivial subgroups of $G$ are
$\mathscr{B}_{\psi}$-groups, then $G$ is a $\mathscr{B}_{\psi}$-group. By
Proposition 2.2, we deduce that $G\cong C_{p^{2}}$ or $exp(G)=p$.

The converse easily follows if one uses Proposition 2.2 and the fact that
$exp(G)=p$ implies that $exp(H)=p$ for any non-trivial subgroup $H$ of $G$.

Let $\pi$ be a set of prime numbers. We recall that a subgroup $H$ of a finite
group $G$ is a Hall $\pi$-subgroup of $G$ if $\pi(H)\subseteq\pi$ and there is
no prime divisor of $[G:H]$ which lies in $\pi$. In what follows, we show that
if a finite group $G$ has a large normal Hall $\pi$-subgroup, then $G$ fails
to be a $\mathscr{B}_{\psi}$-group.

Proposition 2.4. Let $G$ be a finite group and let
$\pi(G)=\\{p_{1},p_{2},\ldots,p_{k}\\}$, where $k\geq 2$ and
$p_{1}<p_{2}<\ldots<p_{k}.$ If $G$ has a normal Hall
$\\{p_{2},p_{3},\ldots,p_{k}\\}$-subgroup, then $G$ is not a
$\mathscr{B}_{\psi}$-group.

Proof. Let $P_{1}$ be a Sylow $p_{1}$-subgroup of $G$ such that
$|P_{1}|=p_{1}^{\alpha}$, where $\alpha\geq 1$. Let $H$ be a normal Hall
$\\{p_{2},p_{3},\ldots,p_{k}\\}$-subgroup of $G$ and $K$ be a subgroup of
$P_{1}$ of order $p_{1}^{\alpha-1}$. Since $H$ is normal, it follows that $HK$
is a maximal subgroup of $G$ of index $p_{1}$. Note that if $x\in H$ and $y\in
HK\setminus H$, then $o(x)\geq p_{2}$ and $o(y)\geq p_{1}$. Then

$\psi(HK)\geq 1+(|H|-1)p_{2}+|H|(|K|-1)p_{1}=|G|+(p_{2}-p_{1})|H|+1-p_{2}>|G|$

since $(p_{2}-p_{1})|H|\geq p_{2}$. We conclude that $G$ is not a
$\mathscr{B}_{\psi}$-group, as desired.

We have the necessary tools to generalize Theorem 1.2 up to the class of
finite nilpotent groups.

Theorem 2.5. Let $G$ be a finite nilpotent group. Then $G$ is a
$\mathscr{B}_{\psi}$-group if and only if $G\cong C_{p^{2}}$ or $exp(G)=p$,
where $p$ is a prime.

Proof. Let $G$ be a finite nilpotent $\mathscr{B}_{\psi}$-group. We take
$\pi(G)=\\{p_{1},p_{2},\ldots,p_{k}\\}$, where $k\geq 1$, and denote by
$P_{i}$ the Sylow $p_{i}$-subgroup of $G$, for all $i\in\\{1,2,\ldots,k\\}$.
Suppose that $k\geq 2$. Since $G$ is the direct product of its Sylow
subgroups, we deduce that $P_{2}P_{3}\ldots P_{k}$ is a normal Hall
$\\{p_{2},p_{3},\ldots,p_{k}\\}$-subgroup of $G$. According to Proposition
2.4, it follows that $G$ is not a $\mathscr{B}_{\psi}$-group, a contradiction.
Then, $k=1$ and $G$ is a finite $p$-group satisfying the $\mathscr{B}_{\psi}$
property. By Proposition 2.2, we conclude that $G\cong C_{p^{2}}$ or
$exp(G)=p$.

As we previously saw, the converse also holds, so the proof is finished.

From now on, we provide some details concerning the non-nilpotent
$\mathscr{B}_{\psi}$\- groups. First of all, we note that Proposition 2.4 is
also useful from a computational point of view, i.e. detecting examples of
non-nilpotent $\mathscr{B}_{\psi}$-groups via GAP [18]. For instance, there
are 398,146,849 non-nilpotent groups of order $1536=2^{9}\cdot 3$. From these
ones, 398,032,384 groups have a normal Sylow 3-subgroup, so they are not
$\mathscr{B}_{\psi}$-groups by Proposition 2.4. The following table outlines
the non-nilpotent $\mathscr{B}_{\psi}$-groups up to order 2000.

Non-nilpotent $\mathscr{B}_{\psi}$-groups $G$ with $1\leq|G|\leq 2000$
---
IdGroup |  Structure Description |  Solvable |  $\pi(G)$
[12, 3] |  $A_{4}$ |  Yes |  $\\{2,3\\}$
[48, 50] |  $C_{2}^{4}\rtimes C_{3}$ |  Yes |  $\\{2,3\\}$
[56, 11] |  $C_{2}^{3}\rtimes C_{7}$ |  Yes |  $\\{2,7\\}$
[60, 5] |  $A_{5}$ |  No |  $\\{2,3,5\\}$
[80, 49] |  $C_{2}^{4}\rtimes C_{5}$ |  Yes |  $\\{2,5\\}$
[120, 5] |  $SL(2,5)$ |  No |  $\\{2,3,5\\}$
[160, 199] |  $((C_{2}\times Q_{8})\rtimes C_{2})\rtimes C_{5}$ |  Yes |  $\\{2,5\\}$
[168, 42] |  $PSL(2,7)$ |  No |  $\\{2,3,7\\}$
[192, 1541] |  $C_{2}^{6}\rtimes C_{3}$ |  Yes |  $\\{2,3\\}$
[320, 1012] |  $(C_{2}^{2}.C_{2}^{4})\rtimes C_{5}$ |  Yes |  $\\{2,5\\}$
[336, 114] |  $SL(2,7)$ |  No |  $\\{2,3,7\\}$
[351, 12] |  $C_{3}^{3}\rtimes C_{13}$ |  Yes |  $\\{3,13\\}$
[360, 118] |  $A_{6}$ |  No |  $\\{2,3,5\\}$
[405, 15] |  $C_{3}^{4}\rtimes C_{5}$ |  Yes |  $\\{3,5\\}$
[448, 178] |  $C_{4}^{3}\rtimes C_{7}$ |  Yes |  $\\{2,7\\}$
[448, 179] |  $(C_{2}^{3}.C_{2}^{3})\rtimes C_{7}$ |  Yes |  $\\{2,7\\}$
[448, 1393] |  $C_{2}^{6}\rtimes C_{7}$ |  Yes |  $\\{2,7\\}$
[448, 1394] |  $C_{2}^{6}\rtimes C_{7}$ |  Yes |  $\\{2,7\\}$
[504, 156] |  $PSL(2,8)$ |  No |  $\\{2,3,7\\}$
[576, 8661] |  $C_{2}^{6}\rtimes C_{9}$ |  Yes |  $\\{2,3\\}$
[660, 13] |  $PSL(2,11)$ |  No |  $\\{2,3,5,11\\}$
[720, 409] |  $SL(2,9)$ |  No |  $\\{2,3,5\\}$
[768, 1085321] |  $C_{2}^{8}\rtimes C_{3}$ |  Yes |  $\\{2,3\\}$
[960, 11357] |  $C_{2}^{4}\rtimes A_{5}$ |  No |  $\\{2,3,5\\}$
[960, 11358] |  $C_{2}^{4}\rtimes A_{5}$ |  No |  $\\{2,3,5\\}$
[992, 194] |  $C_{2}^{5}\rtimes C_{31}$ |  Yes |  $\\{2,31\\}$
[1092, 25] |  $PSL(2,13)$ |  No |  $\\{2,3,7,13\\}$
[1215, 68] |  $((C_{3}\times(C_{3}^{2}\rtimes C_{3}))\rtimes C_{3})\rtimes C_{5}$ |  Yes |  $\\{3,5\\}$
[1280, 1116309] |  $C_{4}^{4}\rtimes C_{5}$ |  Yes |  $\\{2,5\\}$
[1280, 1116310] |  $((C_{2}\times((C_{2}\times((C_{4}\times C_{2})\rtimes C_{2}))\rtimes C_{2}))\rtimes C_{2})\rtimes C_{5}$ |  Yes |  $\\{2,5\\}$
[1280, 1116311] |  $(C_{2}^{4}.C_{2}^{4})\rtimes C_{5}$ |  Yes |  $\\{2,5\\}$
[1280, 1116312] |  $((C_{2}^{2}\times Q_{8})\rtimes Q_{8})\rtimes C_{5}$ |  Yes |  $\\{2,5\\}$
[1280, 1116356] |  $C_{2}^{8}\rtimes C_{5}$ |  Yes |  $\\{2,5\\}$

[1320, 13] |  $SL(2,11)$ |  No |  $\\{2,3,5,11\\}$
---|---|---|---
[1344, 814] |  $C_{2}^{3}.PSL(2,7)$ |  No |  $\\{2,3,7\\}$
[1344, 11686] |  $C_{2}^{3}\rtimes PSL(2,7)$ |  No |  $\\{2,3,7\\}$
[1920, 240998] |  $C_{2}^{5}\rtimes A_{5}$ |  No |  $\\{2,3,5\\}$
[1920, 240999] |  $C_{2}.(C_{2}^{4}\rtimes A_{5})$ |  No |  $\\{2,3,5\\}$
[1920, 241000] |  $C_{2}^{4}\rtimes SL(2,5)$ |  No |  $\\{2,3,5\\}$
[1920, 241001] |  $C_{2}^{5}.A_{5}$ |  No |  $\\{2,3,5\\}$
[1920, 241002] |  $C_{2}^{4}\rtimes SL(2,5)$ |  No |  $\\{2,3,5\\}$

We write some notes based on our enumeration. The list contains only three
non-nilpotent $\mathscr{B}_{\psi}$-group of odd order. Some of the non-
solvable examples are simple or quasisimple groups. In what concerns the non-
nilpotent solvable examples, we observe a similarity: the orders of these
groups have only two prime divisors. Hence, we pose the following open
problem:

Question 1. Let $G$ be a finite non-nilpotent solvable
$\mathscr{B}_{\psi}$-group. Is it true that $|\pi(G)|=2$?

As a consequence of our last observation, one may be interested in studying
the $\mathscr{B}_{\psi}$ property for specific classes of finite groups of
order $p^{\alpha}q^{\beta}$, where $p,q$ are primes and $\alpha\geq
1,\beta\geq 1$. Two such remarkable classes are the finite non-abelian
$P$-groups and the Schmidt groups (i.e. the finite minimal non-nilpotent
groups).

For fixed $p$ and $n$, a remarkable property of the finite $P$-groups is that
they are lattice-isomorphic (see Theorem 2.2.3 of [15]). This is an additional
reason for which we choose to study the $\mathscr{B}_{\psi}$ property of the
$P$-groups. More exactly, if we have two finite non-isomorphic groups $G_{1}$
and $G_{2}$ such that their subgroup lattices are isomorphic and $G_{1}$ is a
$\mathscr{B}_{\psi}$-group, can we conclude that $G_{2}$ has the same
property? The answer is negative since we prove that the only $P$-groups which
satisfy the $\mathscr{B}_{\psi}$ property are the abelian ones.

Corollary 2.6. Let $G$ be a finite $P$-group. Then $G$ is a
$\mathscr{B}_{\psi}$-group if and only if $G$ is elementary abelian.

Proof. Let $G$ be a finite $P$-group. Suppose that $G$ is non-abelian and it
satisfies the $\mathscr{B}_{\psi}$ property. By the description of the non-
abelian $P$-groups, it follows that $G=H\langle x\rangle$, where $H$ is a
normal Sylow $p$-subgroup of $G$ and $o(x)=q$. Since $q|(p-1)$, it follows
that $q<p$ so, according to Proposition 2.4, $G$ would not be a
$\mathscr{B}_{\psi}$-group, a contradiction. Hence $G$ is an abelian
$P$-group, so $G$ is elementary abelian, as desired.

The proof is complete since the converse holds by Theorem 1.2.

We move our attention to studying the $\mathscr{B}_{\psi}$ property of the
Schmidt groups. These are the finite minimal non-nilpotent groups and details
on their properties and structure are covered in [4, 14]. We recall some
aspects as well. If $G$ is a Schmidt group, then $\pi(G)=\\{p,q\\}$, $G$ has a
normal Sylow $p$-subgroup $P$ and a cyclic Sylow $q$-subgroup $Q$. We conclude
that $G=P\rtimes Q$. Moreover, if $r$ is the multiplicative order of $p$
modulo $q$, it is known that if $P$ is abelian, then $P\cong C_{p}^{r}$, while
if $P$ is non-abelian, then $Z(P)=P^{\prime}=\Phi(P)$ is elementary abelian
and $\frac{P}{\Phi(P)}\cong C_{p}^{r}.$ In short, $P$ is a special $p$-group
(p. 183 of [10]). Some constructions of special $p$-groups are covered in [8].
Note that since $\Phi(P)$ and $\frac{P}{\Phi(P)}$ are elementary abelian, it
follows that $exp(P)\in\\{p,p^{2}\\}$. Moreover, according to Theorem 5.2 of
[13], if $p$ is odd, then $exp(P)=p$, while if $p=2$, then $exp(P)=4$.
Finally, if $Q=\langle x\rangle$, then $x^{q}\in Z(G)$. Hence $\langle
x^{q}\rangle$ is a normal subgroup of $G$ which trivially intersects $P$.
Consequently, $G$ has a maximal subgroup $H\cong P\times\langle x^{q}\rangle$
of index $q$. All other maximal subgroups of $G$ are abelian and are of the
form $\Phi(P)Q_{i}$ (see the proof of Theorem 1 of [16]), where
$i\in\\{1,2,\ldots,n_{q}\\}$ and $n_{q}$ is the number of Sylow $q$-subgroups
of $G$. These would be the tools that are necessary to study the
$\mathscr{B}_{\psi}$ property of the Schmidt groups.

Theorem 2.7. Let $G=P\rtimes Q$ be a Schmidt group of order
$p^{\alpha}q^{\beta}$, where $p,q$ are distinct primes and $\alpha\geq
1,\beta\geq 1$. If $G$ is a $\mathscr{B}_{\psi}$-group, then $G=P\rtimes Q$,
where $P$ is a special $p$-group of order $p^{\alpha}$, $Q\cong C_{q}$ and
$p,q$ are primes such that $p<q$. Conversely,

  * i)

if $P$ is abelian, then $G$ is a $\mathscr{B}_{\psi}$-group;

  * ii)

if $P$ is non-abelian, $p$ is odd, $r$ is the order of $p$ modulo $q$, and the
inequality

$\displaystyle(p^{\alpha-r+1}-p+1)(q^{2}-q+1)<p^{\alpha}q$ (1)

holds, then $G$ is a $\mathscr{B}_{\psi}$-group;

  * iii)

if $P$ is non-abelian, $p=2$, $r$ is the order of $p$ modulo $q$, and the
inequalities (1) and

$\displaystyle\psi(P)<2^{\alpha}q$ (2)

hold, then $G$ is a $\mathscr{B}_{\psi}$-group.

Proof. As stated above, $P$ is a normal Sylow $p$-subgroup isomorphic to a
special $p$-group, $Q=\langle x\rangle\cong C_{q^{\beta}}$ and
$H=P\times\langle x^{q}\rangle$ is a maximal subgroup of $G$.

Assume that $G$ is a $\mathscr{B}_{\psi}$-group. Then, by Proposition 2.4, we
have that $p<q$. Also, since $exp(P)\in\\{p,p^{2}\\}$, it follows that
$\psi(P)\geq\psi(C_{p}^{\alpha})$. Using this fact and Lemma 2.1 i) and ii),
we have

$\psi(H)=\psi(P)\psi(C_{q^{\beta-1}})\geq(p^{\alpha+1}-p+1)\cdot\frac{q^{2\beta-1}+1}{q+1}>p^{\alpha}\cdot\frac{q^{2\beta-1}+1}{q+1}.$

If $\beta\geq 3$, then $\frac{q^{2\beta-1}+1}{q+1}>q^{\beta}$, so
$\psi(H)>|G|$, contradicting the $\mathscr{B}_{\psi}$ property of $G$. Hence,
$\beta\in\\{1,2\\}$. If $\beta=2$, according to Lemma 2.1 iii), we deduce that

$\psi(H)=\psi(P)\psi(C_{q})\geq\psi(C_{p}^{\alpha})\psi(C_{q})>p^{\alpha}q^{2},$

a contradiction. Consequently, $G=P\rtimes Q$ is a Schmidt group, where $P$ is
a special $p$-group, $Q\cong C_{q}$ and $p<q$.

Conversely, let $G=P\rtimes Q$ be a Schmidt group of order $p^{\alpha}q$,
where $\alpha\geq 1$, $P$ is a special $p$-group, $Q\cong C_{q}$ and $p,q$ are
primes such that $p<q$.

i) If $P$ is abelian, then the maximal subgroups of $G$ are $P\cong
C_{p}^{\alpha}$ and $Q_{i}\cong C_{q}$, where $i\in\\{1,2,\ldots,n_{q}\\}$.
Also, $\alpha$ would be the multiplicative order of $p$ modulo $q$, so $q\leq
p^{\alpha}-1$. We have

$\psi(P)=\psi(C_{p}^{\alpha})=p^{\alpha+1}-p+1<p^{\alpha+1}<p^{\alpha}q=|G|$

and

$\psi(Q_{i})=\psi(C_{q})=q^{2}-q+1<q^{2}\leq(p^{\alpha}-1)q<p^{\alpha}q=|G|,\
\forall\ i\in\\{1,2,\ldots,n_{q}\\},$

so $G$ is a $\mathscr{B}_{\psi}$-group.

If $P$ is non-abelian, then the maximal subgroups of $G$ are $P$ and
$\Phi(P)Q_{i}\cong C_{p}^{\alpha-r}\times C_{q}$, where
$i\in\\{1,2,\ldots,n_{q}\\}$ and $r$ is the multiplicative order of $p$ modulo
$q$. We distinguish the following two cases based on the parity of $p$.

ii) If $p$ is odd, then $exp(P)=p$. Hence, $\psi(P)=p^{\alpha+1}-p+1<|G|$, as
we previously saw. Assume that $G$ is not a $\mathscr{B}_{\psi}$-group. Then,
there exists $i\in\\{1,2,\ldots,n_{q}\\}$ such that

$\psi(\Phi(P)Q_{i})\geq|G|\Longleftrightarrow\psi(C_{p}^{\alpha-r})\psi(C_{q})\geq|G|\Longleftrightarrow(p^{\alpha-r+1}-p+1)(q^{2}-q+1)\geq
p^{\alpha}q,$

a contradiction. Consequently, $G$ is a $\mathscr{B}_{\psi}$-group.

iii) If $p=2$, then $exp(P)=4$. Assume that $G$ is not a
$\mathscr{B}_{\psi}$-group. Then $\psi(P)\geq|G|$ or there exists
$i\in\\{1,2,\ldots,n_{q}\\}$ such that $\psi(\Phi(P)Q_{i})\geq|G|$. It follows
that

$\psi(P)\geq 2^{\alpha}q\text{ or }(2^{\alpha-r+1}-1)(q^{2}-q+1)\geq
2^{\alpha}q,$

a contradiction. Then $G$ is a $\mathscr{B}_{\psi}$-group and the proof is
complete.

The result given by the case iii) of the previous theorem can be improved if
one explicitly computes $\psi(P)$. Since $P$ would be a special $2$-group with
$exp(P)=4$ and $\Phi(P)\cong C_{2}^{r}$, we can easily get some bounds for
$\psi(P)$ using the fact that the orders of the elements of
$P\setminus\Phi(P)$ belong to $\\{2,4\\}$. More exactly, we get

$2^{\alpha+1}-1<\psi(P)\leq
1+2\cdot(2^{\alpha-r}-1)+4\cdot(2^{\alpha}-2^{\alpha-r}).$

Also, concerning the cases ii) and iii) of the previous theorem, we note that
there are examples of Schmidt groups for which at least one of the
inequalities (1) and (2) hold or not. For instance, $SL(2,3)\cong Q_{8}\rtimes
C_{3}$ is a Schmidt group having a non-abelian kernel $P\cong Q_{8}$ with
$exp(P)=4$. This group is not a $\mathscr{B}_{\psi}$-group since (2) does not
hold: we have $\psi(Q_{8})=27>24=|SL(2,3)|$. Some examples of Schmidt
$\mathscr{B}_{\psi}$-groups $G=P\rtimes Q$, such that $P$ is non-abelian and
$exp(P)=4$, were outlined in our previous table: SmallGroup(160, 199),
SmallGroup(320, 1012). Hence, both groups satisfy inequalities (1) and (2).
Also, from the same table, we can extract SmallGroup(1215, 68) which is a
Schmidt $\mathscr{B}_{\psi}$-group with non-abelian kernel of exponent $3$, so
inequality (1) holds. Finally, it remains unknown if there are any Schmidt
groups, with non-abelian kernel of odd exponent, which are not
$\mathscr{B}_{\psi}$ groups. For instance, if one chooses the quadruple
$(p,q,r,\alpha)=(3,13,3,6)$, inequality (1) is not checked, but the only
Schmidt group of order $9477$ is SmallGroup(9477, 505). However, its structure
description is $C_{13}\rtimes C_{729}$, but we would need a non-abelian kernel
of order 729 in order to follow the hypotheses of Theorem 2.7. Hence, we pose
the following questions related to the last two paragraphs:

Question 2. Let $G$ be a non-abelian special $2$-group. What is the explicit
form of $\psi(G)$?

Question 3. Let $G=P\rtimes Q$ a Schmidt group of order $p^{\alpha}q$, where
$\alpha\geq 1$ and $p,q$ are odd primes such that $p<q$. If $P$ is non-
abelian, is it true that $G$ is a $\mathscr{B}_{\psi}$-group?

If we check our previous table, we observe that $PSL(2,q)$ is a
$\mathscr{B}_{\psi}$-group for $q\in\\{3,4,5,7,8,9,11,13\\}$. For a prime
power $q>3$, it is known that $PSL(2,q)$ is a non-abelian simple group. Hence,
it would be interesting to check if the class consisting of these simple
groups is contained in the class of $\mathscr{B}_{\psi}$-groups. For such a
purpose, a main tool would be Dickson’s classification of the maximal
subgroups of $PSL(2,q)$ (see [9]). One may ask:

Question 4. What can be said about the $\mathscr{B}_{\psi}$ property of the
finite simple groups $PSL(2,q)$?

Finally, other potential $\mathscr{B_{\psi}}$-groups are the $CP_{1}$ groups.
The class of $CP_{1}$ groups consists of all finite groups whose element
orders are primes. Hence, they are some strong candidates for our
investigation. A complete classification of the $CP_{1}$ groups is highlighted
in the main theorem of [7]. Therefore, we suggest a final open problem:

Question 5. What can be said about the $\mathscr{B}_{\psi}$ property of
$CP_{1}$ groups?

A partial answer for this question is given in our paper since the nilpotent
$CP_{1}$ groups are the finite $p$-groups of exponent $p$. These are
$\mathscr{B}_{\psi}$-groups according to Proposition 2.2. The only non-
solvable $CP_{1}$ group is $A_{5}$ which also is a $\mathscr{B}_{\psi}$-group.
Hence, it remains to study the $\mathscr{B}_{\psi}$ property of the non-
nilpotent solvable $CP_{1}$ groups. According to [7], such a group is a
Frobenius group $G=P\rtimes Q$ of order $p^{\alpha}q$, where $p,q$ are primes
and $\alpha\geq 1$. In addition, the kernel $P$ is of exponent $p$.

Acknowledgements. The author is grateful to the reviewers for their remarks
which improve the previous version of the paper. This work was supported by a
grant of the ”Alexandru Ioan Cuza” University of Iasi, within the Research
Grants program, Grant UAIC, code GI-UAIC-2021-01.

Conflict of interest. The author have no conflicts of interest to declare.

Data availability. Data sharing not applicable to this article as no datasets
were generated or analysed during the current study.

## References

  * [1] Amiri, H., Jafarian Amiri, S. M., Isaacs, I.M., Sums of element orders in finite groups, Comm. Algebra 37 (2009), 2978-2980.
  * [2] Amiri, H., Jafarian Amiri, S. M., Sum of element orders on finite groups of the same order, J. Algebra Appl. 10 (2) (2011), 187-190.
  * [3] Bahri, A., Khosravi, B., Akhlaghi, Z., A result on the sum of element orders of a finite group, Arch. Math. 114 (1) (2020), 3-12.
  * [4] Ballester-Bolinches, A., Esteban-Romero, R., Robinson, D. J. S., On finite minimal non-nilpotent groups, Proc. Amer. Math. Soc. 133 (12) (2005), 3455-3462.
  * [5] Baniasad Azad, M., Khosravi, B., A criterion for solvability of a finite group by the sum of element orders, J. Algebra 516 (2018), 115-124.
  * [6] Baniasad Azad, M., Khosravi, B., On two conjectures about the sum of element orders, Canad. Math. Bull. 65 (1) (2022), 30-38.
  * [7] Cheng, K. N., Deaconescu, M., Lang, M. L., Shi, W. J., Corrigendum and addendum to: “Classification of finite groups with all elements of prime order”, Proc. Amer. Math. Soc. 117 (4) (1993), 1205-1207.
  * [8] Cortini, R., On special $p$-groups, Boll. Unione Mat. Ital. Sez. B Artic. Ric. Mat. 8 (3) (1998), 677-689.
  * [9] Dickson, L. E., Linear Groups. With an Exposition of the Galois Field Theory, Dover Publications, New York, 1958.
  * [10] Gorenstein, D., Finite groups, 2nd edition, Chelsea Publishing Co., New York, 1980.
  * [11] Harrington, J., Jones, L., Lamarche, A., Characterizing finite groups using the sum of the orders of the elements, Int. J. Comb. (2014), Art. ID 835125.
  * [12] Herzog, M., Longobardi, P., Maj, M., An exact upper bound for sums of element orders in non-cyclic finite groups, J. Pure Appl. Algebra 222 (7) (2018), 1628-1642.
  * [13] Huppert, B., Endliche Gruppen I, Springer Verlag, Berlin-New York, 1967.
  * [14] Schmidt, O. J., Übber Gruppen, deren sämtliche Teiler spezielle Gruppen sind, Rec. Math. Moscow 31 (1924), 366-372.
  * [15] Schmidt, R., Subgroup lattices of groups, De Gruyter Expositions in Mathematics 14, Walter de Gruyter & Co., Berlin, 1994.
  * [16] Tărnăuceanu, M., Minimal non-Iwasawa finite groups, Results Math. 73 (2018), article ID 143.
  * [17] Tărnăuceanu, M., A criterion for nilpotency of a finite group by the sum of element orders, Comm. Algebra 49 (4) (2021), 1571-1577.
  * [18] The GAP Group, GAP – Groups, Algorithms, and Programming, Version 4.11.0, 2020, https://www.gap-system.org.

Mihai-Silviu Lazorec

Faculty of Mathematics

”Al.I. Cuza” University

Iaşi, Romania

e-mail<EMAIL_ADDRESS>