# Towards the verification of a generic interlocking logic:
Dafny meets parameterized model checking

Alessandro Cimatti  Fondazione Bruno Kessler (FBK<EMAIL_ADDRESS>,  Alberto
Griggio  Fondazione Bruno Kessler (FBK<EMAIL_ADDRESS>and  Gianluca Redondi
Fondazione Bruno Kessler (FBK<EMAIL_ADDRESS>
###### Abstract.

Interlocking logics are at the core of critical systems controlling the
traffic within stations. In this paper, we consider a generic interlocking
logic, which can be instantiated to control a wide class of stations. We
tackle the problem of parameterized verification, i.e. prove that the logic
satisfies the required properties for all the relevant stations. We present a
simplified case study, where the interlocking logic is directly encoded in
Dafny. Then, we show how to automate the proof of an important safety
requirement, by integrating simple, template-based invariants and more complex
invariants obtained from a model checker for parameterized systems. Based on
these positive preliminary results, we outline how we intend to integrate the
approach by extending the IDE for the design of the interlocking logic.

Verification, Interlocking logic, Dafny

††ccs: Software and its engineering Software verification††ccs: Software and
its engineering Model checking††ccs: Software and its engineering System
modeling languages

##  1\. Introduction

Interlocking systems are complex, safety-critical systems controlling the
operation of the devices in a railway station. The main function is the
creation of safe routes for trains from different points in the station. This
requires that the devices insisting upon a given route (e.g. semaphores,
switches, level crossing) must be properly operated and that mutual exclusion
between interfering routes is ensured. At a high level of abstraction, an
interlocking system can be thought of as implementing a very articulated
mutual exclusion protocol, that we refer to as interlocking logic.

In this paper, we investigate the use of a formal approach to ensure the
reliability and integrity of their operations, as a complement to the standard
validation and certification techniques. Our context is an ongoing activity of
RFI (the company managing the Italian railways network), aiming to develop an
in-house, framework to design interlocking logics and support the development
of interlocking systems (Amendola et al., 2020; Cavada et al., 2023). One of
the goals of this framework is to develop a computer-based, in order to go
beyond the current relay-based interlocking technology. Starting from a high-
level controlled natural language to describe the interlocking logic, a model-
based Integrated Development Environment supports the railways signaling
engineers in specifying the interlocking logic in a well-structured and
semantically unambiguous way. Interestingly, the interlocking logic is
_generic_ in that it describes the procedures without specific reference to a
single, given station; rather, it applies to any station in a given class. The
resulting specification is then translated into a SysML model, and from there
compiled into executable code. Then, the user can define a specific station
configuration (e.g. the station of the city of Trento), detailing the exact
number of components and their interactions. Upon configuration, the code can
be tested in a closed loop integration with a yard simulator modeling the
behavior of trains and physical devices.

Formally verifying the interlocking logic is a very important goal, and
several attempts have been made in this direction (Fantechi et al., 2022;
Ferrari and Beek, 2022). On the one side, we attempted to apply software model
checking techniques on the code configured with respect to a specific station.
This approach hit a scalability barrier, due to the sheer size of the
resulting, instantiated model. Even more importantly, the results of the
verification would be applicable to a specific station only. On the other
side, we tried to tackle the problem of verifying the generic interlocking
logic without instantiating it with respect to a specific station. We attempt
to follow an SMT-based approach aiming at devising quantified invariants. This
leads to large and difficult-to-reason-about formulae, due to the lack of a
proper structure.

Based on these experiences, we are investigating an alternative approach, that
leverages the object-oriented features of Dafny to obtain a high-level and
natural framework where we tackle the verification of generic interlocking
logics. We present an artificial but representative case study, that shows how
we intend to model the problem in Dafny and show how we verify some generic
properties. We hint that automation in the verification can be increased by
combining template-based generation of simple invariants and the use of a
parameterized model checker to generate more complex, problem specific
invariants. We believe that the results are quite promising and that the
approach is worth investigating further. We discuss the open challenges that
we still need to solve to make this approach scalable.

##  2\. Developing a Generic Interlocking Logic

In this section, we overview the approach for the development of a generic
interlocking logic (Amendola et al., 2020; Cavada et al., 2023; Amendola et
al., 2022). The development of the interlocking logic is model-based and
starts from a domain-specific controlled natural language (CNL), supported by
the tool AIDA. The interlocking logic is designed through the creation of
_sheets_ , each defining a logical entity, also referred to as a class.
Examples of entities include shunting routes, i.e. the high-level process
devoted to creating a safe path for a train within the station, and lower
level entities such as track segments, switches, level crossing, axal
counters, and semaphores. Each sheet is divided into two parts. The first one
defines the structure of the class, i.e. variables, parameters, and notably
lists of other components that are connected to the class. For example, a
shunting route will have lists of the entities it track segments it insists
upon, e.g. the track segments that must be locked before the green light is
signaled.

The second part of the sheet describes the behavior of the component, which
can be thought of as an extended Finite State Machine. A distinguished state
variable, taking values from an enumerative set, is used to define the current
location in the FSM. Each state transition is characterized by the following
elements:

  * •

Source and Destination;

  * •

Triggers, i.e. events that determine the firing of a transition (e.g. the
reception of a command from an external operator, such as ”create the route
from entrance 3 to platform 12”);

  * •

Guards, i.e. the conditions that must be satisfied to enable a particular
transition. Determinism is ensured by explicitly prioritizing guards;

  * •

Effects: when a transition is executed, effects are applied that alter the
internal state of the component, and possibly the state of components that are
connected to it.

Guards and effects of a transition may read and or write the value of
variables of the objects in the list of the connected components connected to
the class.

The structured natural language used in the sheets has been designed to be
comprehensible even to those not trained in formal languages and incorporates
grammatical structures drawn from domain-specific jargon. Phrases are
structured to ensure traceability to pertinent provisions and regulations. For
instance, an engineer might specify a transition guard as follows: ”Check that
all the track segments of the routes are in a free state.”

In AIDA, the sheets written in controlled natural language are associated with
a number of syntactic and semantic checks and are translated into a SysML
model. From the SysML model, it is possible to extract graphical views of the
FSM for each class. Furthermore, the SysML can be compiled into executable
code (Python and C).

The IDE is complemented by two other tools: TOSCA and Norma. TOSCA implements
a number of functions for the testing of the interlocking logic. It supports
the specification of test scenarios, using a domain specific CNL sharing some
features with the CNL for the interlocking logic. Generic, abstract scenarios
may refer to any specific station and can be automatically instantiated on
concrete scenarios. These can then be run on the suitably instantiated
software, in closed loop with a simulator of the trains and trackside devices.
Automated test case generation oriented to coverage is also supported.

Norma(Amendola et al., 2022) is the tool for the formal analysis of legacy
interlocking systems based on relay technology. The role of Norma is to
extract formulae from the old designs and test that the new specifications
will reflect the behavior of the older systems. The definition of a semantic
correspondence between the two interlocking technologies is nontrivial and
relies on the definition of specific abstractions (Becchi and Cimatti, 2022)
to extract properties to be used in verification.

Within this comprehensive IDE, preliminary experiments in applying formal
verification have been attempted, aiming at proving safety properties of the
generated C code. The tool leverages symbolic model-checking techniques for
software verification, with integration into the Kratos2 model checker
(Griggio and Jonáš, 2023). This approach, however, did not yield the expected
results. On the one hand, even if the generation of C code is generic to all
configurations, its subsequent verification can only take place once the
configuration of a specific station has been provided. This is necessary to
meet the restrictions of Kratos2, that is unable to deal with objects of
unspecified size. As a result, our current capability allows us to assess the
safety of individual stations with regard to specific properties. Furthermore,
the verification of the C implementation of the interlocking logic configured
for a given station incurs scalability problems, due to the large number of
components and their complex connections. For this goal, we could use the
generic generated code as an input for Kratos2, but the invariant generation
engine of the model checker is not able to synthesize the correct
parameterized invariants. Hence, in the rest of this paper, we tackle the
parameterized verification of the _generic_ interlocking logic, without
assuming that a specific station configuration is given.

##  3\. Dafny encoding

The features of the Dafny language support a natural encoding of the
interlocking logic described in previous section. Moreover, the verification
in Dafny is modular, thus possibly reducing the complexity of the system to
verify the single components. We now illustrate a possible Dafny
implementation of a simple example, that has been designed to be
representative and comprehensive of all the constructs of the interlocking
logic. In an ideal scenario, this Dafny code will be generated automatically
from SysML within the IDE, complementing the generation of C and Python code.
Our example consists of a simple station with two kinds of components: tracks,
representing the track segments, and routes, modeling the different routes for
the possible trains.

The track class has two variables: a state variable, and a direction variable,
that is used to simulate the presence of switches. Similarly, the routes have
a state variable and a Boolean one. In addition, each route is connected to a
set of tracks (the ones used by the route), which should be in a particular
direction.

Regarding transitions, we consider for simplicity only one simple method of
the route class, that mirrors the transition from an inactive state to an
active one. The guard corresponds to the condition ‘all the tracks of the
route are in a free state and in the requested direction’, and the effect is
‘assign to all the tracks of the route the state locked’.

In the figures 1 and 2 we can see the two Dafny definitions of the classes. We
start by defining variables, as we would find them in the initial segment of
an AIDA sheet. Subsequently, the methods of the class model the transitions in
the second part of the AIDA sheet. The source and destination states, guards,
and effects of transitions are translated into a series of preconditions and
postconditions for each method. The body of each method is populated with a
representation of the C code generated by AIDA.

⬇

datatype TrackDirection = Straight | Reverse

class Track

{

var state $\colon$ TrackState

var direction $\colon$ TrackDirection

constructor (d $\colon$ TrackDirection)

ensures this.state $=$ TrackState.Init

ensures this.direction $=$ d

{

state $:$$=$ TrackState.Init;

direction $:$$=$ d;

}

method lock()

modifies this

ensures this.state $=$ Locked

ensures this.direction $=$ old(this.direction)

{

this.state $:$$=$ Locked;

}

method go_free()

modifies this

ensures this.state $=$ Free

ensures this.direction $=$ old(this.direction)

{

this.state $:$$=$ Free;

}

method change_dir()

modifies this

ensures this.state $=$ old(this.state)

ensures old(this.direction) $\neq$ this.direction

{

if (this.direction $=$ Straight)

{

this.direction $:$$=$ Reverse;

}

else {

this.direction $:$$=$ Straight;

}

}

}

Figure 1. Dafny encoding of the track class

⬇

datatype RouteState = Init | Active | Wait | Inactive

class Route

{

var state $\colon$ RouteState

var change_dir_request $\colon$ bool

const used $\colon$ seq<Track>

const requested_dir $\colon$ seq<TrackDirection>

ghost predicate ValidRoute()

reads this

{

|this.used| $=$ |this.requested_dir|

}

constructor (u $\colon$ seq<Track>, d$\colon$ seq<TrackDirection>)

requires |u| $=$ |d|

ensures this.state $=$ RouteState.Init

ensures this.requested_dir $=$ d

ensures this.used $=$ u

ensures change_dir_request $=$ false

ensures ValidRoute()

{

used $:$$=$ u;

requested_dir $:$$=$ d;

state $:$$=$ RouteState.Init;

change_dir_request $:$$=$ false;

}

method activateroute()

modifies this, this.used[..]

requires ValidRoute()

requires this.state $=$ Wait

requires $\forall$ t $\bullet$ t in this.used $\Longrightarrow$ t.state $=$
Free

requires $\forall$ i $\bullet$ 0 $\leq$ i < |this.used| $\Longrightarrow$

this.used[i].direction $=$ this.requested_dir[i]

ensures ValidRoute()

ensures this.state $=$ Active

ensures this.change_dir_request $=$

old(this.change_dir_request)

ensures ($\forall$ t $\bullet$ t in this.used

$\Longrightarrow$ t.state $=$ Locked)

ensures ($\forall$ t $\bullet$ t in this.used

$\Longrightarrow$ t.direction $=$ old(t.direction))

{

var i $:$$=$ 0;

while i < |this.used|

modifies this.used[..]

invariant 0 $\leq$ i $\leq$ |this.used|

invariant $\forall$ t $\bullet$ t in this.used[..i]

$\Longrightarrow$ t.state $=$ Locked

invariant $\forall$ t $\bullet$ t in this.used

$\Longrightarrow$ t.direction $=$ old(t.direction)

{

this.used[i].lock();

i $:$$=$ i + 1;

}

this.state $:$$=$ Active;

}

}

Figure 2. Dafny encoding of the route class

We remark that, unlike the description of the AIDA sheet, the formalization of
the methods in Dafny introduces a ”modifies” clause. Additionally, we must
explicitly include equalities among variables that remain unchanged in the
postconditions. The initial challenge in automating Dafny code generation lies
in accurately representing these statements.

Up to this point, the verification checks performed by Dafny are focused on
ensuring that the generated code complies with the specified requirements. The
only invariants required for this verification occur in the while loop of the
‘activate route’ method. We suppose that we can generate such invariants
automatically, without the need of an external tool, as they reflect the
structure of the generated code, which is under our control.

Lastly, we introduce the concluding segment of the Dafny code designed for
verifying the safety of the station, in figure 3.

⬇

include ”routes.dfy”

class Station

{

const routes $\colon$ set<Route>

const tracks $\colon$ set<Track>

ghost predicate ValidStation()

reads this, this.routes

{

$\land$ this.routes $\neq$ {}

$\land$ this.tracks $\neq$ {}

$\land$ ($\forall$ i $\bullet$ i in this.routes $\Longrightarrow$

($\exists$ j $\bullet$ j in this.tracks $\land$ j in i.used))

$\land$ ($\forall$ i, t $\bullet$ i in this.routes $\land$

t in i.used $\Longrightarrow$ t in this.tracks)

$\land$ $\forall$ r $\bullet$ r in routes $\Longrightarrow$ r.ValidRoute()

}

ghost predicate NotCompatibleRoutes(a $\colon$ Route,

b $\colon$ Route)

reads a, b

{

($\exists$ i $\bullet$ (i in a.used) $\land$ (i in b.used)) $\land$ a $\neq$ b

}

ghost predicate SecureStation ()

reads this, this.routes

{

$\forall$ i,j $\bullet$ (i in this.routes) $\land$

(j in this.routes) $\land$ (NotCompatibleRoutes(i,j))

$\Longrightarrow$ $\lnot$(i.state $=$ Active $\land$ j.state $=$ Active)

}

ghost predicate SecureInductiveStation()

reads this, this.tracks, this.routes

{

this.SecureStation() $\land$

$\forall$ r, t $\bullet$ (r in this.routes $\land$ t in this.tracks

$\land$ t in r.used $\land$ t.state $=$ Free)

$\Longrightarrow$ $\lnot$ (r.state $=$ Active)

}

predicate Precondition(r $\colon$ Route)

requires r.ValidRoute()

reads r, r.used

{

$\land$ ($\forall$ t $\bullet$ t in r.used

$\Longrightarrow$ t.state $=$ Free)

$\land$ ($\forall$ i $\bullet$ 0 $\leq$ i < |r.used|

$\Longrightarrow$ r.used[i].direction $=$

r.requested_dir[i])

}

method StationScheduler()

modifies this.routes, this.tracks

requires ValidStation()

requires SecureInductiveStation()

ensures ValidStation()

ensures SecureInductiveStation()

decreases *

{

while true

modifies this.routes, this.tracks

invariant ValidStation()

invariant SecureInductiveStation()

decreases *

{

var r $\colon$| r in this.routes;

match r.state {

case Init $\Rightarrow$ r.deactivate();

case Inactive $\Rightarrow$ r.requestroute();

case Wait $\Rightarrow$ if Precondition(r)

{r.activateroute();}

case Active $\Rightarrow$ r.deactivateroute()}

}

}

}

Figure 3. Dafny encoding of the station

Within this last code segment, we introduce the concept of a station, which is
portrayed as a collection of routes and tracks. Subsequently, we define the
station’s scheduler, a crucial element in the system. This scheduler
nondeterministically selects a method that can be executed and proceeds with
its execution.

Additionally, we define the property that we seek to validate, named ”Secure
Station,” which corresponds to the property ‘two incompatible routes cannot be
active together’.

The loop of the scheduler tries to establish that the property is preserved by
each method. Notably, this preservation is not true for the initial property
itself, ”Secure Station.” However, the verification succeeds when we provide a
stronger inductive invariant that implies the original property - called
”Secure Inductive Station”.

The goal of this project would be to use a parameterized model checker to find
these inductive invariants automatically.

##  4\. Invariant inference with a Parameterized Model Checker

Parameterized model checking is a verification technique designed to assess
whether a given property holds true for all possible system configurations,
making it particularly valuable for systems with variable sizes or structures.
This approach allows for the analysis of system behavior, safety, and
correctness across a range of instances, providing a formal framework for
universal reliability. Unfortunately, with the exception of a few cases,
parameterized verification is undecidable. Nonetheless, in the literature,
there are various approaches that can automatically synthesize invariants for
parameterized systems (Ghilardi and Ranise, 2010; Cimatti et al., 2022, 2021;
Abdulla et al., 2018). In particular, the algorithm presented in (Cimatti et
al., 2022) is an SMT-based algorithm for the verification of parameterized
systems. In that setting, unbounded components are modeled via a theory of a
simple type, and state variables are functions from such types to other
theories.

Our goal is to use such a model checker to synthesize automatically the
inductive invariants that Dafny needs to conclude the proof. We illustrate the
main concepts of SMT-based parameterized model checking continuing the last
example. To formalize the whole system symbolically, we need to define a
transition system $S=(X,I(X),T(X,X^{\prime}))$, where $X$ is a set of
variables, and $I,T$ are formulas over some theory. A key insight here is that
we do not need to represent all the attributes of the class, but only the one
relevant to building the inductive invariant. In this example, we have
obtained this simplification manually, by selecting the variables that were
more significant. Ideally, such a selection should be done automatically by
some kind of slicing abstraction, guided by domain-based intuitions.

For this example, the only variables we need are two state variables, one with
sort $track\mapsto\\{free,locked\\}$ and one with sort
$route\mapsto\\{active,inactive\\}$. The initial formula of the system is:

$\forall t:track.(state[t]=free)\wedge\forall r:route.(state[r]=inactive).$

Moreover, we model the dependencies between a route and its associated tracks
with a binary predicate $UsedBy$ with sort $route\times state\mapsto Bool$.
The method ‘activate route’ can thus be modeled with the following formula:

$\exists r:route\big{(}state[r]=inactive\wedge\\\ \forall
t1:track(Usedby(t1,r)\rightarrow state[t1]=free)\wedge\\\ {}\wedge
state^{\prime}[r]=active\wedge\forall s:route(s\neq r\rightarrow
state^{\prime}[s]=state[s])\\\ {}\wedge\forall t:track.(Usedby(t,r)\rightarrow
state^{\prime}[t]=locked\\\ \wedge\neg Usedby(t,r)\rightarrow
state^{\prime}[t]=state[t])\big{)}.$

Then, we define

$NotCompatible(r1,r2)\iff\\\ r1\neq r2\wedge\exists t:track.Usedby(t,r1)\wedge
Usedby(t,r2),$

and the candidate property, represented by the formula:

$\forall r1,r2:route\big{(}NotCompatible(r1,r2)\rightarrow\\\
\neg(state[r1]=active\wedge state[r2]=active)\big{)}.$

using the (implementation of the) algorithm of (Cimatti et al., 2022), we can
find (in less than one second) the lemma

$\forall r:route,t:track(Usedby(t,r)\wedge state[t]=free)\\\
\rightarrow(state[r]\neq active)$

which, in conjunction with the original property, is an inductive invariant
for $S$. This is the same invariant as the ‘Secure Inductive Station’ in the
Dafny code of the station. It’s important to highlight that the symbolic
system $S$ represents a simplified version of the station. In this simplified
example, both tracks and routes contain fewer variables compared to their
original counterparts.

This straightforward illustration portrays an ideal scenario where Dafny and a
parameterized model checker seamlessly collaborate to arrive at a conclusive
proof. Without Dafny, the typical approach would require monolithic use of the
model checker, but this approach often struggles to scale effectively when
dealing with exceptionally large models.

##  5\. Ongoing and Future Work

We tackle the problem of formally verifying an interlocking logic expressed in
a domain specific language. The main problem is that the logic is
parameterized, in the sense that it is intended to control any station with an
arbitrary number of components. We preliminarily analyzed a highly simplified
case study, with two main insights. First, we confirm that it is possible to
directly encode the main features of the interlocking logic in Dafny in a very
natural way. Second, we investigate verification and the relation to simple
invariants (from predefined schemata) and to more complex invariants
(resulting from the application of parameterized model checker (Cimatti et
al., 2022)).

Given the successful preliminary steps, we intend to extend the IDE for the
Interlocking logic to support parameterized verification. The first step will
be to devise an encoder to automatically generate Dafny code automatically
from SysML. We expect this step to be relatively simple, given that the
interlocking logic constructs have a direct correspondence to Dafny ones, and
back-and-forth traceability can be achieved. The Dafny code will incorporate
both the method bodies, mirroring the C and Python code, and the preconditions
and postconditions, echoing the engineers’ natural language specifications.
Second, we will integrate a way to express the properties to be proved, likely
leveraging the language for specifying the abstract scenarios in the TOSCA
environment (Amendola et al., 2020). Third, we will integrate the generation
of invariants required to show that the interlocking logic satisfies the
expected properties. On the one side, we will instrument the encoding to
automatically generate ”simple” invariants via templates, to check the
compliance of the generated code to specification. On the other, we will
integrate a parameterized model checker (and possibly other invariant
generators) to infer invariants for general safety properties of the
interlocking logic.

For the latter, we anticipate a more complex path. Parameterized model
checkers are not designed for tackling large-scale problems. Hence, our plan
is to utilize them on smaller abstractions derived from the code. After the
abstraction is built, we are not interested in finding immediately an
invariant: even if the parameterized model checker takes hours to synthesize a
good invariant, we would be satisfied. However, the most hard challenge will
likely be finding the correct abstractions. It could be possible to explore
the notion of guiding this abstraction process with insights gained from
failed verifications. Extracting such insights from the Dafny verification
conditions may be arduous, as the formulae generated by Boogie might be
cryptic. As a result, we think that the design of the abstraction-refinement
loop should be conducted outside the realm of Dafny.

Furthermore, we do not dismiss the idea of a semi-automated approach, where
railway engineers can contribute lemmas or provide guidance in the abstraction
process, potentially in controlled natural language.

## References

  * (1)
  * Abdulla et al. (2018) Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. 2018.  _Model Checking Parameterized Systems_.  Springer International Publishing, Cham, 685–725.  https://doi.org/10.1007/978-3-319-10575-8_21
  * Amendola et al. (2022) Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella, and Marco Zamboni. 2022.  NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 125–142.
  * Amendola et al. (2020) Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Giuseppe Scaglione, Angelo Susi, Alberto Tacchella, and Matteo Tessi. 2020.  A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System. In _Leveraging Applications of Formal Methods, Verification and Validation: Applications_ , Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 240–254.
  * Becchi and Cimatti (2022) Anna Becchi and Alessandro Cimatti. 2022.  Abstraction Modulo Stability for Reverse Engineering. In _Computer Aided Verification_ , Sharon Shoham and Yakir Vizel (Eds.). Springer International Publishing, Cham, 469–489.
  * Cavada et al. (2023) Roberto Cavada, Alessandro Cimatti, Alberto Griggio, and Angelo Susi. 2023.  A Formal IDE for Railways: Research Challenges. In _Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops_ , Paolo Masci, Cinzia Bernardeschi, Pierluigi Graziani, Mario Koddenbrock, and Maurizio Palmieri (Eds.). Springer International Publishing, Cham, 107–115.
  * Cimatti et al. (2021) Alessandro Cimatti, Alberto Griggio, and Gianluca Redondi. 2021.  Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. In _Automated Deduction – CADE 28_ , André Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham, 131–147.
  * Cimatti et al. (2022) Alessandro Cimatti, Alberto Griggio, and Gianluca Redondi. 2022.  Verification of SMT Systems with Quantifiers. In _Automated Technology for Verification and Analysis_ , Ahmed Bouajjani, Lukáš Holík, and Zhilin Wu (Eds.). Springer International Publishing, Cham, 154–170.
  * Fantechi et al. (2022) Alessandro Fantechi, Gloria Gori, Anne E. Haxthausen, and Christophe Limbrée. 2022.  Compositional Verification of Railway Interlockings: Comparison of Two Methods. In _Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification_ , Simon Collart-Dutilleul, Anne E. Haxthausen, and Thierry Lecomte (Eds.). Springer International Publishing, Cham, 3–19.
  * Ferrari and Beek (2022) Alessio Ferrari and Maurice H. Ter Beek. 2022.  Formal Methods in Railways: A Systematic Mapping Study.  _ACM Comput. Surv._ 55, 4, Article 69 (nov 2022), 37 pages.  https://doi.org/10.1145/3520480
  * Ghilardi and Ranise (2010) Silvio Ghilardi and Silvio Ranise. 2010.  MCMT: A Model Checker Modulo Theories. In _Automated Reasoning_ , Jürgen Giesl and Reiner Hähnle (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 22–29.
  * Griggio and Jonáš (2023) Alberto Griggio and Martin Jonáš. 2023.  Kratos2: An SMT-Based Model Checker for Imperative Programs. In _Computer Aided Verification_ , Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland, Cham, 423–436.


# Detecting Extraneous Content in Podcasts

Sravana Reddy
Spotify
<EMAIL_ADDRESS>
&Yongze Yu
Spotify
<EMAIL_ADDRESS>
&Aasish Pappu
Spotify
<EMAIL_ADDRESS>
Aswin Sivaraman11footnotemark: 1
Indiana University
<EMAIL_ADDRESS>
&Rezvaneh Rezapour
University of Illinois
at Urbana-Champaign
<EMAIL_ADDRESS>
&Rosie Jones
Spotify
<EMAIL_ADDRESS>∗ Work done while at Spotify

###### Abstract

Podcast episodes often contain material extraneous to the main content, such
as advertisements, interleaved within the audio and the written descriptions.
We present classifiers that leverage both textual and listening patterns in
order to detect such content in podcast descriptions and audio transcripts. We
demonstrate that our models are effective by evaluating them on the downstream
task of podcast summarization and show that we can substantively improve ROUGE
scores and reduce the extraneous content generated in the summaries.

##  1 Introduction

Podcasts are a rich source of data for speech and natural language processing.
We consider two types of textual information associated with a podcast
episode: the short description written by the podcast creator, and the
transcript of its audio, both of which may contain content that is not
directly related to the main themes of the podcasts. Such content may come in
the form of sponsor advertisements, promotions of other podcasts, or mentions
of the speakers’ websites and products.

While such content is tightly integrated into the user experience and
monetization, it is a source of noise for many natural language processing and
information retrieval applications which utilize podcast data. For example
(Table 1), an episode of the podcast show Survival includes a promotion for an
unrelated podcast Dog Tales about dogs; a search query for podcasts on dogs
should probably not surface the Survival episode. Algorithms attempting to
connect topics discussed in the podcast to those mentioned in the episode
description, such as summarization models, would be confounded by the presence
of supplementary material and URLs in the description. Information extraction
models looking for entities may mistakenly retrieve sponsor names from
advertisements.

… sit stay and roll over with excitement for par casts endearing series dog
tails. Listen to dog tails free on Spotify or wherever you get your podcast.
And now back to the story. Almost immediately after setting sail on June 29th.
1871 Charles Francis Halls Arctic Expedition…
---
… the focus is on strengthening deficient repertoires, while systematically
increasing task demands and difficulty. For more information, visit
www.behaviorbabe.com. — This episode is sponsored by Anchor: The easiest way
to make a podcast. https://anchor.fm/app
Table 1: Portions of a podcast transcript and episode description which
contain extraneous material (in bold).

In this paper, we introduce the problem of detecting extraneous content (which
we sometimes shorthand as EC) in episode descriptions and audio transcripts.
We produce an annotated corpus by taking advantage of podcast listening data,
construct models to detect extraneous content, and evaluate our models for
accuracy of detection, as well as for the downstream task of summarizing
podcast transcripts. We also discuss some of challenges that arise while
annotating and classifying extraneous content in this domain.

##  2 Previous Work

A related, well-studied problem is boilerplate detection on web pages, mainly
involving the detection of templates, navigational elements, and
advertisements Kohlschütter et al. (2010). Such models tend to rely on the
specific structure of web page boilerplate markup and characteristics. There
has also been work on detecting promotional content on Wikipedia Bhosale et
al. (2013).

There are primarily two lines of work in advertisement detection and discovery
in multimedia. One computes acoustic features over the entire audio to
discriminate between the segments of content and the segments of
advertisements Conejero and Anguera (2008); Melamed and Kim (2009); Nguyen et
al. (2010). The other fuses multimodal features such as visual cues to segment
ad clips from televised and online videos Lienhart et al. (1997); Duan et al.
(2006); Vedula et al. (2017). Our work is closely related to Huang et al.
(2018), who analyze consumer engagement on audio advertisements when compared
to topical content, as we utilize the user engagement signals to predict
extraneous content segments.

##  3 Datasets and Annotation

To create an annotated dataset, we selected a random set of podcast episodes
out of the Spotify Podcast Dataset, a corpus of $105,360$ episodes Clifton et
al. (2020); Jones et al. (2020). Each episode in the dataset has an
automatically generated transcript and a short text description of the episode
written by the podcast creators. We annotate both sources, creating ground-
truth labels for the extraneous content detection task, using the open source
software doccano Nakayama et al. (2018). Annotators were instructed to select
spans that correspond to extraneous content, which we defined as ads, social
media links, promotions of other podcasts, and show notes that are not
directly related to the episode. Respecting sentence boundaries was
encouraged, but not required, to allow for cases where extraneous content
starts or ends mid-sentence.

###  3.1 Podcast Episode Descriptions

Annotation of episode descriptions was relatively straightforward. We
encountered a few corner cases: for example, an episode may in its entirety be
a promotion or an ad; a description that reflects these promotions would be
on-topic. In such scenarios, the annotations attempted to be consistent with
the annotators’ judgments of the main topics of the episode as far as
possible. Examples of annotated episode descriptions are shown in Table 6 in
the appendix.

###  3.2 Podcast Episode Transcripts

Each transcript contains thousands of words, of which extraneous content may
make up a small portion. This necessitates a way to sample an informative
subset of transcript segments for annotation. We observe that if a region is
extraneous to the main content, listeners of the podcast episode may fast-
forward past this region or abandon listening. To this end, we gather listener
data for a subset of our corpus from Spotify, an audio streaming platform. We
record the proportion of all listeners who begin streaming an episode retained
at each second of the episode’s duration. Listening data was aggregated from
the date of each episode’s publication – with the most recent episode
published in February 2020 – through September 2020. For episodes with a
substantial number of listeners, there exist distinct local minima or “dips”
in the retention curves (Figure 1), which we posit may correspond to regions
of extraneous content.

Figure 1: A podcast listener retention curve for a single podcast episode. The
dips in the graph suggest potential EC regions. Start- and end-points for each
dip are automatically estimated as described in Section 3.2, shown with green
and red markers respectively.

To locate the center point of each dip, we first apply SciPy peak detection on
the negative retention curve Virtanen et al. (2020). Within $\pm
2\text{\,}\min$ of each peak, we calculate the slopes of secant lines passing
through every point on the curve. The coordinates which maximize the secant
slope within this range correspond to the start/end points of the dips. Green
and red secant lines are shown in Figure 1 to illustrate this process.

The transcript is then segmented $60\text{\,}\sec$ before the starting point
and $90\text{\,}\sec$ after the ending point of each dip, loosening the
boundaries of the potential EC regions; these segments are then manually
annotated. We note that the transcripts contain noisy text which are artifacts
from an automatic speech recognition (ASR) system. An additional challenge
stems from identifying native advertising, where podcast creators deliberately
script product placement into the context of their content Einstein (2015);
Hutton (2015). Considering all cases, we attempted to best estimate the
boundaries of the scripted content.

Examples of annotated transcript regions are shown in Table 7 in the appendix.
The set of manual annotations is used as a gold labeled transcript dataset for
our models.

Of the annotated dips, $38.4\text{\,}\mathrm{\char 37\relax}$ were found not
to contain extraneous content. These largely correspond to episode beginnings,
where listeners may skip over the introduction to show, or dynamically
inserted ads that are not present in the transcript. The dip boundaries for
the rest are relatively accurate against the manual annotations, with an
absolute mean error of $16.0$ words for the starts, and $35.2$ for the ends,
motivating the use of the un-annotated listener dips as a silver training set
(described in §4.2).

#### Sentence-Level Labels

Our models for descriptions and transcripts use the sentence as the unit of
classification. The annotated data is split into sentences using
SpaCy111https://spacy.io. A sentence is labeled as extraneous if more than
$50\text{\,}\mathrm{\char 37\relax}$ is annotated as such (Table 2).

Dataset | # of episodes | # of sentences
---|---|---
Episode Descriptions | 1730 (61.58% w/ EC) | 10410 (43.80% w/ EC)
Transcripts (Gold) | 506 (62.25% w/ EC) | 12918 (24.01% w/ EC)
|  |

Table 2: Our manually annotated datasets show that the majority of podcast
episodes do contain extraneous content, making up a sizeable fraction of all
sentences.

##  4 Extraneous Content Detection

###  4.1 Sentence-Level Classification

We built separate classifiers for detecting extraneous content in descriptions
and transcripts. A pre-trained BERT Devlin et al. (2019) cased language
model222https://huggingface.co/bert-base-cased was first fine-tuned on our
entire large corpus (of podcast descriptions and transcripts respectively,
excluding the test set) to capture the distinctive language use of the podcast
domain, and then further fine-tuned for classification on the annotated data
to predict whether a sentence is extraneous. We also trained non-neural
classifiers (logistic regression and SVMs) with TF-IDF unigram and bigram
features (Appendix A.2).

We experimented with single sentence classification in isolation, and with the
immediately preceding sentence prepended for context.333The two sentences are
concatenated. In BERT, we include the SEP token to separate them. Where there
is no preceding sentence, we use a special __START__ token.

#### Results

Our experiments used a training/test split of $90$/$10$ for annotated
transcripts and $80$/$20$ for episode descriptions. The best results come from
BERT where the model sees the previous sentence (Table 3). We observed that
classification precision and recall are comparable on the descriptions
dataset; however, with transcripts, precision tends to be lower ($0.690$) than
recall ($0.870$). This suggests that the model mistakenly identifies sentences
as extraneous, but has fairly good coverage. This seems to be because many
sentences in extraneous content in the training transcripts are seemingly
innocuous when taken out of context, confounding the model during training.

|  | Single Sentence | Sentence with Context
---|---|---|---
Dataset | Model | Unigram | Bigram | Unigram | Bigram
Episode Descriptions | LR | 0.893 | 0.818 | 0.858 | 0.850
SVM | 0.907 | 0.907 | 0.898 | 0.896
BERT | 0.920 | 0.940
Transcripts (Gold) | LR | 0.651 | 0.603 | 0.629 | 0.638
SVM | 0.675 | 0.679 | 0.663 | 0.670
BERT | 0.710 | 0.769
|  |  |  |  |

Table 3: F1 score of three sentence-level EC classifiers tested across two
datasets.

Dataset |  Model | Doc. (%) | Sen. (%)
---|---|---|---
Episode Descriptions |  Sentence-level BERT | 86.4 | 94.9
BERT + Change Point | 89.6 | 95.4
BERT + BiLSTM-CRF | 87.6 | 95.0
Transcripts (Gold) |  Sentence-level BERT | 43.1 | 88.7
BERT + Smoothing | 49.1 | 90.9
Transcripts (Silver) |  Sentence-level BERT | 60.8 | 96.6
BERT + Smoothing | 66.7 | 97.0
|  |  |

Table 4: Classification accuracy of sentence-level and document-level
extraneous content detection. Documents come from either the dataset of full
episode descriptions, or from transcript segments corresponding to dip
regions. A document EC-match occurs when all sentence labels agree; this is
difficult to achieve with longer segments.

###  4.2 Document-Level Classification

We classify sentences independently, but extraneous content comes as
contiguous groups of sentences. We apply non-parametric kernel regression to
post-hoc smooth the sequence of individual sentence classification
probabilities in the transcripts. We observe that extraneous content within
episode descriptions often appears as a contiguous block at the end, prompting
us to apply a change point detector (Appendix A.3) on the sentence
classification probabilities in order to detect the start of the EC block.

We also formulate the problem as sequence tagging at the sentence level, in
order to allow the model to learn the label dependencies. For this, we use the
BERT pooled sentence embeddings as input to a separate BiLSTM-CRF model. The
BiLSTM-CRF improves over sentence-level classification but underperforms the
change point detection strategy (Table 4). In future work, we would like to
investigate an end-to-end BERT-BiLSTM-CRF model Dai et al. (2019) or
sequential sentence classification models Cohan et al. (2019).

#### Expanded Transcript Dataset

Since the manually labeled gold set is small, we create a larger silver
dataset from $6401$ detected listener dips across $4930$ episodes by applying
the best performing classifier trained on the gold data. To encode information
about the dip locations to aid the model, we prepend special tokens ‘in-dip’
and ‘outside-dip’ to each sentence depending on whether the sentence lies
within a listening dip.

We strip special tokens from the resulting silver set. This data is then used
to train a final classifier that can detect extraneous content regions in
podcast transcripts without listener dips. We also add a negative sample of
sentences that are distant (by at least 5 minutes) from dips in the same
episodes, with the assumption that these are likely to be topical.

On the same test set as the previous experiments, the document and sentence
level performance increases (Table 4), proving the model benefits from the
larger, albeit noisy, training set. This model is applied to the corpus in the
downstream task described below.

##  5 Application to Podcast Summarization

We address the problem of automatically generating episode descriptions from
podcast transcripts, a task similar to abstractive summarization. Within this
problem, we evaluate the downstream effect of removing extraneous sentences
from the training and/or test data. Alternatives to removal (such as using the
model’s predictions as auxiliary inputs in the downstream system) are left for
future work.

We experiment with two supervised abstractive summarization models both built
using BART Lewis et al. (2020). The first experiment uses a model pretrained
for summarization on the CNN/DailyMail
dataset444https://huggingface.co/facebook/bart-large-cnn Hermann et al.
(2015). This model (which we refer to as BART-CNN) evaluates the extent to
which extraneous text in the transcripts contribute to the presence of
extraneous content in the generated descriptions. In the second experiment, we
fine-tune BART-CNN on our corpus of podcasts, similar to the work of Zheng et
al. (2020), using the episode transcripts as inputs and descriptions as
targets. We refer to this model as BART-Podcasts; with it, we can evaluate the
effects of EC as realistic noise which may contaminate the training data of
summarization models.

###  5.1 Experimental Setup

From the original corpus of $105,360$ podcast shows, $6401$ were used for
training and evaluation of the two EC detection models. We filter the
remaining episodes for descriptions which are distinctly short or long. The
resulting dataset contains $84,451$ episodes sorted by episode publication
date. This is split into $82,451$ episodes for training, $1000$ for
validation, and $1000$ for evaluation.

As a baseline, we manually remove extraneous content from the episode
descriptions within the test set, comparing the Rouge score of the model
outputs against the manually-cleaned descriptions as well as against the
original descriptions. Additionally, we manually validate whether the
generated outputs for $150$ random test episodes contain extraneous content.

Model |  EC Removal Method |  Rouge-L against original descriptions |  Rouge-L against cleaned descriptions |  Amount of EC in output (%)
---|---|---|---|---
| Rec. | Pre. | F | Rec. | Pre. | F
Original Descriptions
(no model) | n/a | 1.000 | 1.000 | 1.000 | 0.996 | 0.810 | 0.872 | 50.0
BART-CNN | n/a | 0.310 | 0.199 | 0.204 | 0.340 | 0.170 | 0.195 | 18.8
| M1 | 0.299 | 0.200 | 0.199 | 0.330 | 0.172 | 0.192 | 11.5
| M2 | 0.309 | 0.188 | 0.195 | 0.345 | 0.165 | 0.191 | 4.0
BART-Podcasts | n/a | 0.377 | 0.329 | 0.315 | 0.349 | 0.228 | 0.248 | 73.2
| M1 | 0.269 | 0.309 | 0.247 | 0.308 | 0.280 | 0.260 | 8.7
| M3 | 0.323 | 0.276 | 0.261 | 0.367 | 0.247 | 0.263 | 15.5
| M4 | 0.330 | 0.281 | 0.269 | 0.376 | 0.261 | 0.268 | 2.0
|  |  |  |  |  |  |  |
Table 5: Evaluation of the effect of extraneous content detection on a
downstream summarization task. Accuracies are reported in terms of recall,
precision, and F1 score. The models are provided with data pre-processed
through one of four EC removal strategies: (M1) cleaned test descriptions,
(M2) cleaned test transcripts, (M3) cleaned training descriptions, or (M4)
cleaned descriptions and transcripts for both train and test.

###  5.2 Results

Table 5 shows the full Rouge-L scores of our experiments. We evaluate quality
through Rouge as well as by manually verifying for the presence of extraneous
content in the outputs. BART-CNN is an out of the box summarization model,
while BART-Podcasts is the same model that is fine-tuned on our data of
transcripts and descriptions. All numbers are reported on the test split of
the corpus. The range of these Rouge scores is comparable to previous podcast
summarization work. Removing extraneous content is clearly beneficial for
summary quality: while the baseline models have better Rouge scores against
the original (EC-containing) descriptions, the highest scoring models score
better against the clean descriptions compared to the originals. With the
original data, both BART-CNN and BART-Podcasts tend to generate descriptions
that contain extraneous material. Interestingly, BART-Podcasts, being trained
on the unmodified descriptions, produces even more extraneous content
($73.2\text{\,}\mathrm{\char 37\relax}$) than the corresponding original
descriptions ($50.0\text{\,}\mathrm{\char 37\relax}$), often generating ads
unrelated to the actual sponsors, and nonexistent URLs. While post-processing
only the output summaries with no change to the model inputs is effective at
minimizing extraneous content, it does so at the expense of summary quality,
since the resulting summaries are significantly shortened. The best overall
performance comes from detecting extraneous content on transcripts and
descriptions before model training and application.

##  6 Conclusion

We introduced the problem of detecting extraneous content in podcast
descriptions and transcripts, presented models that leverage textual and
listener data, and evaluated them on a downstream summarization task.

We consider our models to be baselines for a new problem with several
opportunities for future work. Although we used two separate models for the
descriptions and transcripts with the view that the language patterns are
different, a joint model or shared components may be able to take advantage of
some of the common vocabulary. One could leverage the ‘boilerplate’ nature of
some types of extraneous content like ads by detecting repeated sentences and
phrases across the corpus. A language model that is robust to noisy speech
transcripts Lin et al. (2019); Chuang et al. (2019) may improve accuracy on
podcast transcripts. Given that extraneous content may appear as pre-recorded
audio, or with a different speaking pitch and cadence, acoustic features
alongside textual ones may be helpful.

##  7 Acknowledgments

We thank Ann Clifton and Jussi Karlgren for valuable assistance with the
summarization model and evaluations, Richard Mitic, Laurence Pascall, Skylar
Brannon, Kristie Savage, and Karishma Gulati for collaborating on identifying
listening dips from user logs, Iftekhar Tanveer for helpful discussions, and
the anonymous EACL reviewers for their suggestions.

## References

  * Bhosale et al. (2013) Shruti Bhosale, Heath Vinicombe, and Raymond Mooney. 2013.  Detecting promotional content in Wikipedia.  In _Proceedings of the 2013 Conference on Empirical Methods in Natural Language Processing_ , pages 1851–1857, Seattle, Washington, USA. Association for Computational Linguistics.
  * Chuang et al. (2019) Yung-Sung Chuang, Chi-Liang Liu, and Hung-Yi Lee. 2019.  Speechbert: Cross-modal pre-trained language model for end-to-end spoken question answering.  _arXiv preprint arXiv:1910.11559_.
  * Clifton et al. (2020) Ann Clifton, Sravana Reddy, Yongze Yu, Aasish Pappu, Rezvaneh Rezapour, Hamed Bonab, Maria Eskevich, Gareth Jones, Jussi Karlgren, Ben Carterette, and Rosie Jones. 2020.  100,000 podcasts: A spoken English document corpus.  In _Proceedings of the 28th International Conference on Computational Linguistics_ , pages 5903–5917, Barcelona, Spain (Online). International Committee on Computational Linguistics.
  * Cohan et al. (2019) Arman Cohan, Iz Beltagy, Daniel King, Bhavana Dalvi, and Dan Weld. 2019.  Pretrained language models for sequential sentence classification.  In _Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP)_ , pages 3693–3699, Hong Kong, China. Association for Computational Linguistics.
  * Conejero and Anguera (2008) David Conejero and Xavier Anguera. 2008.  Tv advertisements detection and clustering based on acoustic information.  In _2008 International Conference on Computational Intelligence for Modelling Control & Automation_, pages 452–457. IEEE.
  * Dai et al. (2019) Zhenjin Dai, Xutao Wang, Pin Ni, Yuming Li, Gangmin Li, and Xuming Bai. 2019.  Named entity recognition using bert bilstm crf for chinese electronic health records.  In _2019 12th International Congress on Image and Signal Processing, BioMedical Engineering and Informatics (CISP-BMEI)_ , pages 1–5. IEEE.
  * Devlin et al. (2019) Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. 2019.  BERT: Pre-training of deep bidirectional transformers for language understanding.  In _Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short Papers)_ , pages 4171–4186, Minneapolis, Minnesota. Association for Computational Linguistics.
  * Duan et al. (2006) Ling-Yu Duan, Jinqiao Wang, Yantao Zheng, Jesse S Jin, Hanqing Lu, and Changsheng Xu. 2006.  Segmentation, categorization, and identification of commercial clips from tv streams using multimodal analysis.  In _Proceedings of the 14th ACM international conference on Multimedia_ , pages 201–210.
  * Einstein (2015) Brandon R. Einstein. 2015.  Reading Between the Lines: The Rise of Native Advertising and the FTC’s Inability to Regulate It.  _Brook. J. Corp. Fin. & Com. L._, 10:225.
  * Hermann et al. (2015) Karl Moritz Hermann, Tomas Kocisky, Edward Grefenstette, Lasse Espeholt, Will Kay, Mustafa Suleyman, and Phil Blunsom. 2015.  Teaching machines to read and comprehend.  In C. Cortes, N. D. Lawrence, D. D. Lee, M. Sugiyama, and R. Garnett, editors, _Advances in Neural Information Processing Systems 28_ , pages 1693–1701. Curran Associates, Inc.
  * Huang et al. (2018) Jason Huang, David Reiley, and Nick Riabov. 2018.  Measuring consumer sensitivity to audio advertising: A field experiment on pandora internet radio.  _Available at SSRN 3166676_.
  * Hutton (2015) Christopher Hutton. 2015.  Podcasting embraces native advertising.
  * Jones et al. (2020) Rosie Jones, Ben Carterette, Ann Clifton, Maria Eskevich, Gareth Jones, Jussi Karlgren, Aasish Pappu, Sravana Reddy, and Yongze Yu. 2020.  Overview of the TREC 2020 Podcasts Track.  In _The 29th Text Retrieval Conference (TREC 2020) notebook_. NIST.
  * Kohlschütter et al. (2010) Christian Kohlschütter, Peter Fankhauser, and Wolfgang Nejdl. 2010.  Boilerplate detection using shallow text features.  In _Proceedings of the third ACM international conference on Web search and data mining_ , pages 441–450.
  * Lewis et al. (2020) Mike Lewis, Yinhan Liu, Naman Goyal, Marjan Ghazvininejad, Abdelrahman Mohamed, Omer Levy, Veselin Stoyanov, and Luke Zettlemoyer. 2020.  BART: Denoising sequence-to-sequence pre-training for natural language generation, translation, and comprehension.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 7871–7880, Online. Association for Computational Linguistics.
  * Lienhart et al. (1997) Rainer Lienhart, Christoph Kuhmunch, and Wolfgang Effelsberg. 1997.  On the detection and recognition of television commercials.  In _proceedings of IEEE international Conference on Multimedia Computing and Systems_ , pages 509–516. IEEE.
  * Lin et al. (2019) H. Lin, T. Lo, and B. Chen. 2019.  Enhanced bert-based ranking models for spoken document retrieval.  In _2019 IEEE Automatic Speech Recognition and Understanding Workshop (ASRU)_ , pages 601–606.
  * Melamed and Kim (2009) I Dan Melamed and Yeon-Jun Kim. 2009.  Automatic detection of audio advertisements.  In _Tenth Annual Conference of the International Speech Communication Association_.
  * Nakayama et al. (2018) Hiroki Nakayama, Takahiro Kubo, Junya Kamura, Yasufumi Taniguchi, and Xu Liang. 2018\.  doccano: Text annotation tool for human.  Software available from https://github.com/doccano/doccano.
  * Nguyen et al. (2010) MN Nguyen, Qi Tian, and Ping Xue. 2010.  Efficient advertisement discovery for audio podcast content using candidate segmentation.  _EURASIP Journal on Audio, Speech, and Music Processing_ , 2010(1):1–12.
  * Vedula et al. (2017) Nikhita Vedula, Wei Sun, Hyunhwan Lee, Harsh Gupta, Mitsunori Ogihara, Joseph Johnson, Gang Ren, and Srinivasan Parthasarathy. 2017.  Multimodal content analysis for effective advertisements on youtube.  In _2017 IEEE International Conference on Data Mining (ICDM)_ , pages 1123–1128. IEEE.
  * Virtanen et al. (2020) Pauli Virtanen, Ralf Gommers, Travis E. Oliphant, Matt Haberland, Tyler Reddy, David Cournapeau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, Stéfan J. van der Walt, Matthew Brett, Joshua Wilson, K. Jarrod Millman, Nikolay Mayorov, Andrew R. J. Nelson, Eric Jones, Robert Kern, Eric Larson, C J Carey, İlhan Polat, Yu Feng, Eric W. Moore, Jake VanderPlas, Denis Laxalde, Josef Perktold, Robert Cimrman, Ian Henriksen, E. A. Quintero, Charles R. Harris, Anne M. Archibald, Antônio H. Ribeiro, Fabian Pedregosa, Paul van Mulbregt, and SciPy 1.0 Contributors. 2020.  SciPy 1.0: Fundamental Algorithms for Scientific Computing in Python.  _Nature Methods_ , 17:261–272.
  * Wolf et al. (2020) Thomas Wolf, Lysandre Debut, Victor Sanh, Julien Chaumond, Clement Delangue, Anthony Moi, Pierric Cistac, Tim Rault, Rémi Louf, Morgan Funtowicz, Joe Davison, Sam Shleifer, Patrick von Platen, Clara Ma, Yacine Jernite, Julien Plu, Canwen Xu, Teven Le Scao, Sylvain Gugger, Mariama Drame, Quentin Lhoest, and Alexander M. Rush. 2020.  Transformers: State-of-the-art natural language processing.  In _Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing: System Demonstrations_ , pages 38–45, Online. Association for Computational Linguistics.
  * Zheng et al. (2020) Chujie Zheng, Harry Jiannan Wang, Kunpeng Zhang, and Ling Fan. 2020.  A baseline analysis for podcast abstractive summarization.

##  Appendix A Appendix

###  A.1 Annotation Process and Annotated Examples

Examples of extraneous content regions of episode descriptions are shown in
Table 6. and example of annotated listener ‘dip’ regions in the podcast
transcripts in Table 7. The categorization into types is only for illustrative
purposes and is not used in our model.

Type |  Examples
---|---
Platform Ads |  Transformation Church Pastor Mike Todd brings Marked Part 8- You Are Enough \--- This episode is sponsored by Anchor: The easiest way to make a podcast. https://anchor.fm/app Support this podcast: https://anchor.fm/m-e8/support
Social media links, podcast promotions, sponsor ads |  Crazy new years news, Dallin fantasizes about a Tesla, and then we do some hilarious Mad Libs… you have to hear these. Follow the Dashleys for more! https://thedashleysxxxx.com https://facebook.com/thedashleysxxx https://instagram.com/thedashxxxx https://youtube.com/thedasxxxx<EMAIL_ADDRESS>Check out our new Podcast! http://anchor.fm/takingsxxxx Thank you to Skillshare for sponsoring this podcast! Get 2 months premium membership free here: skillshare.com/dashxxxx Thank you to HelloFresh for sponsoring this podcast! Sign up for HelloFresh and get 10 free meals here! URL: hellofresh.com/BIGLITTLELIxxx Promo: BIGLITTLELxxxx — Support this podcast: https://anchor.fm/biglittlexxxx/support
Table 6: Annotated examples from episode descriptions. (Some of the links are masked for privacy.) Type |  Subtype |  Examples
---|---|---
Sponsorships
/ Ads |  Products |  … the railway tracks a mere four inches a small but deadly act of sabotage. Hey friend, I want to tell you about the new $3 Little John from Jimmy John’s […] or with the Jimmy John’s app at participating locations taxes and delivery fees extra. Welcome to today and True Crime a par cast original…
|  Platforms |  … before we move on to your next topic. We just want to say thanks to our sponsor Anchor. If you haven’t heard about Anchor […] and it’s everything you need to make a podcast in one place download the free anchor app or go to Anchor. Um to get started, a very somber…
Podcast
Promotions |  Other
Podcasts |  … Coming up heading returns to Denmark and Begins the long journey to reclaim his throne. Darkness tragedy pain these things hide within every beloved institution and most people are none the wiser every week. […] Search The Dark Side of or visit Park ask.com / Dark Side to listen now. Now back to the story…
|  Social
Media |  … manipulates our relationships into deadly results at par cast we are grateful for you our listeners you allow us to do what we love let us know how we’re doing reach out on Facebook and Instagram at par cast and Twitter […] for more information. It all began with a computer…
Not EC |  Episode
Introduction |  … I’m your host Taylor structure of the live Daily Talk Radio Show […] It’s getting to meet interesting inspiring and exceptional people and getting them to talk about the heaviest things in the world. So if you love real talk with a…
|  Miscellaneous
Content |  … Not much is known about her personal life prior to her murder if she was so average, why was she living with her aunt and uncle I’m not saying there’s anything wrong with that […] I’m sorry to say that it looks as though your husband has an advanced…
Table 7: Annotated examples from the podcast transcripts, corresponding to
detected dips in listening.

###  A.2 Model Training and Evaluation Details

We modified the sentence splitter in SpaCy to include \---, ... and the three-
space string as delimiters for episode descriptions, based on our observations
of common patterns. Speech recognition errors/disfluencies and missing
punctuation contribute to a small amount of noise in the sentence
segmentations of transcripts and descriptions respectively.

For the bag of words models, we used https://scikit-learn.org/ implementations
with the default parameters and no hyper-parameter tuning.

For all Transformer models, we used the Huggingface library Wolf et al.
(2020). For summarization, we set the maximum length of the target
descriptions as 250 tokens for training and generation, and the minimum length
to 30 tokens. The models were trained for up to 5 epochs, with early stopping
based on ROUGE-2 on the validation set. All other hyperparameters were set as
the defaults specified in the Huggingface Transformers code.

For evaluation, we use the Files2Rouge implementation
(https://github.com/pltrdy/files2rouge), after tokenizing both the reference
and the outputs using the Moses tokenizer
(https://github.com/alvations/sacremoses).

###  A.3 Change Point Detection for Episode Descriptions

As shown in Eq. 1, we can find a position $\hat{\tau}$ which maximizes the
negative log-likelihood ratio $\textit{R}_{\tau}$ of $\textit{H}_{1}$ as the
existence of the change point versus $\textit{H}_{0}$ as no change point.

$\hat{\tau}=\displaystyle\arg\max_{\begin{subarray}{c}1\leq\tau\leq
N\end{subarray}}\textit{R}_{\tau}$ (1)

We make the assumption that $(1)$ there is only one change point, and $(2)$
extraneous content appears at end the descriptions. The null hypothesis is
that there is no changepoint, while the alternative hypothesis assumes that
there is a changepoint at the time $t=\tau$. Here is the hypothesis test:

$H_{0}:\theta_{1}=\theta_{2}=...=\theta_{N-1}=\theta_{N}\\\ $ (2)
$H_{1}:\theta_{1}=...=\theta_{\tau-1}=\theta_{\tau}\neq\theta_{\tau+1}=...=\theta_{N}$
(3)

Therefore, the likelihood is given by the probability of observation the data
$x$ = $x_{1}$,…,$x_{n}$ conditional on $H_{0}$. In other words,

$\emph{L}(\textit{H}_{0})=p(x|\textit{H}_{0})=\prod_{i=1}^{N}p(x_{i}|\theta_{i})$
(4)

And the the likelihood of the alternative hypothesis is,

$\emph{L}(\textit{H}_{0})=p(x|\textit{H}_{1})=\prod_{i=1}^{\tau}p(x_{i}|\theta_{i})\prod_{j=\tau+1}^{N}p(x_{j}|\theta_{j})$
(5)

The log-likelihood ratio ${R_{\tau}}$ is then,

$\begin{split}\textit{R}_{\tau}&=\log{\frac{\emph{L}_{\textit{H}_{0}}}{\emph{L}_{\textit{H}_{1}}}}\\\
&=\sum_{i=1}^{\tau}\log{p(x_{i}|\theta_{1})}+\sum_{j=\tau+1}^{N}\log{p(x_{j}|\theta_{2})}\\\
&\quad-\sum_{k=1}^{N}\log{p(x_{k}|\theta_{0})}\end{split}$ (6)


#  Quasi-pure resolutions and some lower bounds of Hilbert coefficients of
Cohen-Macaulay modules.

Tony J. Puthenpurakal<EMAIL_ADDRESS>and  Samarendra Sahoo
<EMAIL_ADDRESS>Department of Mathematics, IIT Bombay, Powai, Mumbai
400 076, India

###### Abstract.

Let $(A,\mathfrak{m})$ be a Gorenstein local ring and let $M$ be a finitely
generated Cohen Macaulay $A$ module. Let $G(A)=\bigoplus_{n\geq
0}\mathfrak{m}^{n}/\mathfrak{m}^{n+1}$ be the associated graded ring of $A$
and $G(M)=\bigoplus_{n\geq 0}\mathfrak{m}^{n}M/\mathfrak{m}^{n+1}M$ be the
associated graded module of $M$. If $A$ is regular and if $G(M)$ has a quasi-
pure resolution then we show that $G(M)$ is Cohen-Macaulay. If $G(A)$ is
Cohen-Macaulay and if $M$ has finite projective dimension then we give lower
bounds on $e_{0}(M)$ and $e_{1}(M)$. Finally let $A=Q/(f_{1},\ldots,f_{c})$ be
a strict complete intersection with $\operatorname{ord}(f_{i})=s$ for all $i$.
Let $M$ be an Cohen-Macaulay module with $\operatorname{cx}_{A}(M)=r<c$. We
give lower bounds on $e_{0}(M)$ and $e_{1}(M)$.

###### Key words and phrases:

Associated graded rings and modules, strict complete intersections, Gorenstein
rings, graded resolutions

###### 1991 Mathematics Subject Classification:

Primary 13A30, 13C14; Secondary 13D40, 13D07

##  1\. Introduction

Let $(A,\mathfrak{m})$ be a Cohen Macaulay local ring of dimension $d$ with
residue field $k=A/\mathfrak{m}$ and let $M$ be finitely generated $A$-module.
Let $G(A)=\bigoplus_{n\geq 0}\mathfrak{m}^{n}/\mathfrak{m}^{n+1}$ be the
associated graded ring of $A$ and $G(M)=\bigoplus_{n\geq
0}\mathfrak{m}^{n}M/\mathfrak{m}^{n+1}M$ be the associated graded module of
$M$ considered as a graded $G(A)$-module. Let $\lambda(E)$ denotes length of
an $A$-module $E$. Let $M$ be an $A$-module of dimension $r$ . The Hilbert
series of $M$ is

$H_{M}(z)=\sum_{i\geq
0}\lambda(\mathfrak{m}^{i}M/\mathfrak{m}^{i+1}M)z^{i}=\frac{h_{M}(z)}{(1-z)^{r}}.$

Where $h_{M}(z)=h_{0}+h_{1}z+\ldots+h_{t}z^{t}$ is called $h$-polynomial of
$M$. The integer $e_{i}(M)=h^{i}_{M}(1)$ is called as the $i^{th}$-Hilbert
coefficient of $M$, where $h^{i}_{M}(z)$ is $i$-th derivative of $h_{M}(z).$

I: _The case when $A$ is regular local._

Let $A=K[[x_{1},\ldots,x_{n}]]$ be a power series ring over the field $K$ and
$M$ be a Cohen-Macaulay $A$-module. In [11] the author proved that if $G(M)$
has a pure resolution then $G(M)$ is Cohen Macaulay. When $A$ is not
equicharacteristic this result is proved in [1].

Let $R$ be a standard graded polynomial ring over a field and $E$ be a
finitely generated graded $R$ module. Define

$\alpha_{i}=\operatorname{max}\\{n\,|\,\operatorname{Tor}_{i}(k,E)_{n}\neq
0\\}$

and

$\gamma_{i}=\operatorname{min}\\{n\,|\,\operatorname{Tor}_{i}(k,E)_{n}\neq
0\\}.$

We say $E$ has a pure resolution if $\alpha_{i}=\gamma_{i}$ for all $i\geq 0$
and quasi pure resolution if $\gamma_{i}\geq\alpha_{i-1}$ for all $i\geq 1.$
For examples of pure and quasi-pure resolution see 3.5.

Our first result is:

######  Theorem 1.1.

Let $(A,\mathfrak{m})$ be a regular local ring and $M$ be a Cohen Macaulay $A$
module. Set $R=G(A)=k[X_{1},\ldots,X_{n}]$. Set
$p=\operatorname{projdim}(G(M))$. If $G(M)$ is not Cohen Macaulay then
$\alpha_{p}(M)<\alpha_{p-1}(M).$

An easy application of this theorem is:

######  Corollary 1.2.

Let $(A,\mathfrak{m})$ be a regular local ring and $M$ be a finitely generated
Cohen Macaulay $A$ module. If $G(M)$ has quasi-pure resolution then $G(M)$ is
Cohen Macaulay.

II: _Cohen-Macaulay modules with finite projective dimension._

If $A$ is not regular then note that even if $\operatorname{projdim}_{A}M$ is
finite it might very well happen that $\operatorname{projdim}_{G(A)}G(M)$ is
infinite. For an example if $A$ is Cohen-Macaulay with $0ptG(A)=0$ then
$\operatorname{projdim}_{G(A)}G(M)$ is infinite if $\dim M<\dim A$. However if
$A$ is Gorenstein and $G(A)$ is Cohen-Macaulay then if $M$ is a Cohen-Macaulay
module with finite projective dimension then we can give bounds of
multiplicity $e_{0}(M)$ and the first Hilbert coefficient $e_{1}(M)$ of $M$.
Let $\operatorname{reg}(G(A))$ denote the regularity of $G(A)$. We prove

######  Lemma 1.3.

Let $(A,\mathfrak{m})$ be a Gorenstein local ring. Assume $G(A)$ is Cohen
Macaulay. Let $M$ be an Cohen Macaulay module of dimension $r$ with finite
projective dimension. Then $e_{0}(M)\geq\mu(M)+c$ and
$e_{1}(M)\geq\binom{c+1}{2},$ where $c=\operatorname{reg}(G(A)).$

We also show that if the lower bound for $e_{1}(M)$ is attained then
necessarily $G(M)$ is Cohen-Macaulay, see Theorem 4.3.

III: _Cohen-Macaulay modules over strict complete intersections._

Next, we consider the following situation. Let $(Q,\mathfrak{n})$ be a regular
local ring with infinite residue field,
$f_{1},\ldots,f_{c}\in\mathfrak{n}^{2}$ of order $s$ such that
$f_{1}^{*},\ldots,f_{c}^{*}$ is a $G(Q)$-regular sequence. Let
$A=Q/(f_{1},\ldots,f_{c})$ and let $M$ be an Cohen Macaulay $A$-module with
$\operatorname{cx}_{A}(M)=r<c$.

######  Theorem 1.4.

(with hypotheses as above) Then $e_{0}(M)\geq\mu(M)+\alpha$ and
$e_{1}(M)\geq\binom{\alpha+1}{2}$, where $\alpha=(c-r)(s-1).$ Moreover if
$e_{1}(M)=\binom{\alpha+1}{2}$ then $G(M)$ is Cohen Macaulay.

We now describe in brief the contents of this paper. In section 2 we describe
some preliminary results that we need. In section 3 we sketch a proof of
Theorems 1.1 and Corollary 1.2. We also give some examples showing that our
hypothesis about $M$ is optimal. In section 4 we give a proof of Lemma 1.3.
Finally, in section five we prove Theorem 1.4.

##  2\. Preliminaries

Throughout this paper all rings considered are Noetherian and all modules
considered (unless stated otherwise) are finitely generated.

######  2.1.

Let $(A,\mathfrak{m})$ be a local ring and let $M$ be an $A$-module. Define
$L(M)=\bigoplus_{n\geq 0}M/\mathfrak{m}^{n+1}M$. Let
$\mathcal{R}=A[\mathfrak{m}t]$ be Rees ring and
$\mathcal{R}(M)=\bigoplus_{n\geq 0}\mathfrak{m}^{n}Mt^{n}$ be Rees module of
$M$. The Rees ring $\mathcal{R}$ is a subring of $A[t]$. So $A[t]$ is an
$\mathcal{R}$ module. Therefore $M[t]=M\otimes_{A}A[t]$ is an
$\mathcal{R}$-module. The exact sequence

$0\to\mathcal{R}(M)\to M[t]\to L(M)(-1)\to 0$

defines an $\mathcal{R}$ module structure on $L(M)(-1)$ and hence on
$L(M)$(for more details see ([9], definition 4.2)). Note that $L(M)$ is not a
finitely generated $\mathcal{R}$-module.

######  2.2.

An element $x\in\mathfrak{m}$ is called $M$-superficial with respect to
$\mathfrak{m}$ if there exists $c\in\mathbb{N}$ such that for all $n\geq c$,
$(\mathfrak{m}^{n+1}M:_{M}x)\cap\mathfrak{m}^{c}M=\mathfrak{m}^{n}M$. If depth
$M>0$ then one can show that a $M$-superficial element is $M$-regular.
Furthermore $(\mathfrak{m}^{n+1}M:_{M}x)=\mathfrak{m}^{n}M$ for $n\gg 0.$
Superficial elements exist if the residue field is infinite.

A sequence $x_{1},\ldots,x_{r}$ in $(A,\mathfrak{m})$ is said to be
$M$-superficial sequence if $x_{1}$ is $M$-superficial and $x_{i}$ is
$M/(x_{1},\ldots,x_{i-1})M$-superficial for $2\leq i\leq r.$

######  2.3.

Let $x_{1},\ldots,x_{n}$ be a sequence in $A$. For an $A$-module $M$, we
denote $K\textbf{.}(\underline{x},M)$ as Koszul complex of $\underline{x}$
with respect to $M$ and $H_{i}(K\textbf{.}(\underline{x},M))$ as it’s $i$-th
homology group.

Let $\underline{x}=x_{1},\ldots,x_{n}$ be a sequence in $A$ and $M$ is an
$A$-module. Comparing the $i$-th homology groups
$H_{i}(K\textbf{.}(\underline{x},M))$ and
$H_{i}(K\textbf{.}(x^{\prime},M))(\text{where
}x^{\prime}=x_{1},\ldots,x_{n-1})$, we get the following short exact sequence,
for all $i\geq 0$

$0\to H_{0}(x_{n},H_{i}(K\textbf{.}(x^{\prime},M)))\to
H_{i}(K\textbf{.}(\underline{x},M))\to
H_{1}(x_{n},H_{i-1}(K\textbf{.}(x^{\prime},M)))\to 0.$

######  2.4.

(Sally Descent)  Let $(A,\mathfrak{m})$ be local ring, $M$ an $A$-module of
dimension $d$. Let $x_{1},\ldots,x_{r}$ is an $M$-superficial sequence with
$r<d$. Set $B=A/(x_{1},\ldots,x_{r})$ and $N=M/(x_{1},\ldots,x_{r})M$. Then

$\operatorname{depth}_{G(B)}G(N)\geq
1\operatorname{iff}\operatorname{depth}_{G(A)}G(M)\geq r+1.$

##  3\. Length of $i$-th Koszul homology of associated graded modules

In this section $\mathcal{R}$ denotes the Rees ring $A[\mathfrak{m}t]$.

######  Theorem 3.1.

Let $(A,\mathfrak{m})$ be a Cohen Macaulay local ring with an infinite residue
field. $M$ be a finitely generated Cohen Macaulay $A$ module of dimension
$r\geq 1$. Let $Xt=x_{1}t,\ldots,x_{r}t\in\mathcal{R}_{1}.$ Then
$\lambda(H_{i}(Xt,L(M)))<\infty,\text{ for all }i\geq 1$, where
$\underline{x}=x_{1},\ldots,x_{r}$ is an $M$-superficial sequence.

###### Proof.

We will prove this by induction on $r$. Set $L=L(M)$. Let $r=1$. We have an
exact sequence

($\star$) ${}0\to\mathcal{B}(x_{1},M)\to L(M)(-1)\xrightarrow{\phi}L(M)\to
L(N)\to 0,$

where $\phi(a+\mathfrak{m}^{n}M)=x_{1}a+\mathfrak{m}^{n+1}M$,
$\mathcal{B}(x_{1},M)=\bigoplus_{n\geq
0}(\mathfrak{m}^{n+1}M:x_{1}/\mathfrak{m}^{n}M)$ and $N=M/x_{1}M$. From above
exact sequence, we get $H_{1}(x_{1}t,L(M))=\bigoplus_{n\geq
0}(\mathfrak{m}^{n+1}M:x_{1}/\mathfrak{m}^{n}M).$ Since $x_{1}$ is
$M$-superficial regular $(\mathfrak{m}^{n+1}M:x_{1})/\mathfrak{m}^{n}M=0$ for
$n\gg 0.$ Hence
$\lambda(H_{1}(x_{1}t,L(M)))<\infty.$ Now assume it is true for $r=s$. we have

$0\to H_{0}(x_{s+1}t,H_{i}(X^{\prime}t,L))\to H_{i}(Xt,L)\to
H_{1}(x_{s+1}t,H_{i-1}(X^{\prime}t,L)\to 0,$

where $X^{\prime}=x_{1},\ldots,x_{s}$. By induction
$\lambda(H_{i}(Xt,L(M)))<\infty$ for all $i\geq 2$. Since
$H_{0}(X^{\prime}t,L(M))=L(M/X^{\prime}M)$ and as $x_{s+1}$ is
$M/X^{\prime}M$-superficial, by $(\star)$ we get
$H_{1}(x_{s+1},H_{0}(X^{\prime}t,L(M)))$ has finite length. Hence
$\lambda(H_{i}(Xt,L(M)))<\infty$ for all $i\geq 1.$ ∎

Next we prove

######  Lemma 3.2.

Let $(A,\mathfrak{m})$ be a regular local ring with an infinite residue field.
$M$ be a Cohen Macaulay $A$-module of dimension $r$. Let $x_{1},\ldots,x_{r}$
be a $M\oplus A$-superficial sequence. Then $H_{i}(Xt,Yt,L(M))\text{ for all
}i>s$ has finite length, where $X=x_{1},\ldots,x_{r}$ is $M$-superficial
sequence and $\mathfrak{m}=<x_{1},\ldots,x_{r},y_{1},\ldots,y_{s}>$(minimal
set of generators).

###### Proof.

Set $L=L(M)$. We will prove that $H_{i}(Xt,y_{1}t,\ldots,y_{l}t,L)$ has finite
length for $i>l$ by induction on $l$. Let $l=1$. We have the following short
exact sequence

$0\to H_{0}(y_{1}t,H_{i}(Xt,L))\to H_{i}(Xt,y_{1}t,L)\to
H_{1}(y_{1}t,H_{i-1}(Xt,L))\to 0.$

By Theorem 3.1, we get for all $i\geq 2>1$, $H_{i}(Xt,y_{1}t,L)$ has finite
length. Now assume it is true for $l=c.$ Similarly as above we have the
following short exact sequence

$0\to H_{0}(y_{c+1}t,H_{i}(Xt,Y^{\prime}t,L))\to H_{i}(Xt,Yt,L)\to
H_{1}(y_{c+1}t,H_{i-1}(Xt,Y^{\prime}t,L))\to 0,$

where $Y^{\prime}=y_{1},\ldots,y_{c}.$ Since for $i>c$,
$H_{i}(Xt,y_{1}t,\ldots,y_{c}t,L)$ has finite length. So for $i>c+1$,
$H_{i}(Xt,y_{1}t,\ldots,y_{c+1}t,L)$ has finite length. ∎

The main result of this section is:

######  Theorem 3.3.

Let $(A,\mathfrak{m})$ be a regular local ring of dimension $d$ and let $M$ be
a Cohen Macaulay $A$-module. Set $R=G(A)=k[X_{1},\ldots,X_{d}]$. Set
$p=\operatorname{projdim}(G(M))$. If $G(M)$ is not Cohen Macaulay then
$\alpha_{p}(M)<\alpha_{p-1}(M).$

###### Proof.

We may assume the residue field of $A$ is infinite. Let the dimension of $M$
is $r$ and $x_{1},\ldots,x_{r}$ be a $M\oplus A$-superficial sequence with
respect to $\mathfrak{m}.$ Since $A$ is regular with infinite residue field,
so $x_{1},\ldots,x_{r}$ is part of regular system of parameters of $A$. Let
$\mathfrak{m}=\langle x_{1},\ldots,x_{r},y_{1}\ldots,y_{l}\rangle$ be minimal
set of generator. Here $1\leq r\leq d-1$, so $l\geq 1.$ Let depth
$G(M)=c<r(0\leq c\leq r).$ If $c\geq 1$ then $x^{*}_{1},\ldots,x^{*}_{c}$ is
$G(M)$ regular(see [8], Theorem 8) and

$G(M)/(x_{1}^{*},\ldots,x_{c}^{*})G(M)\cong G(M/(x_{1},\ldots,x_{c})M).$

Set $N=M/(x_{1},\ldots,x_{c})M$ and
$S=G(A/(x_{1},\ldots,x_{c}))=R/(x_{1}^{*},\ldots,x_{c}^{*}).$ We also have
$\operatorname{Tor}^{R}_{i}(k,G(M))\cong\operatorname{Tor}^{S}_{i}(k,G(N))$
for all $i$(see [7], p-140). So we can now assume depth $G(M)=0.$ dim$M=\text{
dim }G(M)=r\geq 1$ and dim$A=d=r+l\geq r+1.$

We have a short exact sequence

$0\to G(M)\to L(M)\to L(M)(-1)\to 0.$

This induces the following exact sequence

$0\to H_{d}(Xt,Yt,G(M))\to H_{d}(Xt,Yt,L(M))\to
H_{d}(Xt,Yt,L(M)(-1))\to\ldots.$

Set $V_{i}=H_{i}(Xt,Yt,G(M))$ and $W=H_{d}(Xt,Yt,L(M))$. From above exact
sequence we get

$0\to V_{d,n}\to W_{n}\to W_{n-1}\to V_{d-1,n}\to\ldots.$

We know $V_{d-1,n}=0$ for all $n\geq\alpha_{p-1}(M)+1.$ So for all
$n\geq\alpha_{p-1}(M)+1$ we get surjections

$W_{n+3}\twoheadrightarrow W_{n+2}\twoheadrightarrow W_{n+1}\twoheadrightarrow
W_{n-1}\to 0.$

Since $r\geq 1$ and $d=r+l>l$. By Lemma 3.2, the length of
$W=H_{d}(Xt,Yt,L(M))$ is finite. So $W_{n+j}=0\text{ for all }j\gg 0.$ Thus
$W_{j}=0\text{ for }j\geq\alpha_{p-1}.$ So $V_{d,j}=0\text{ for all
}j\geq\alpha_{p-1}.$ Hence $\alpha_{p}(M)<\alpha_{p-1}(M).$

∎

As a consequence we get:

######  Corollary 3.4.

(With hypothesis as in 3.3) If $G(M)$ has a quasi-pure resolution then $G(M)$
is Cohen Macaulay.

###### Proof.

Suppose $G(M)$ is not Cohen Macaulay. Set $p=\operatorname{projdim}(G(M))$. By
above theorem $\alpha_{p}<\alpha_{p-1}.$ But $G(M)$ has quasi pure resolution,
so $\alpha_{p}\geq\gamma_{p}\geq\alpha_{p-1}.$ This is a contradiction. ∎

We give some examples which show our assumptions are optimal. We used Singular
[5] to check the following examples.

######  Example 3.5.

  1. (1)

Let $A=k[[x,y]]$, $I=(x^{2},xy)$ and $M=A/I$. It is clear that $M$ is not
Cohen Macaulay and is of dimension 1. Note $G(M)=R/(X^{2},XY)$, where
$R=k[X,Y]$. Now we have the following pure graded resolution of $G(M)$

$0\to R(-3)\to R^{2}(-2)\to R\to 0.$

Here $\alpha_{2}=3$ and $\alpha_{1}=2$, $i.e.$ $\alpha_{2}>\alpha_{1}.$

  2. (2)

Let $A=k[[x,y]]$ and $M=k.$ Then $G(M)=k$ is Cohen Macaulay. From the Koszul
complex of $G(M)$ we get $\alpha_{i}=i\text{ for all }i,\,1\leq i\leq d.$ This
implies $\alpha_{d}>\alpha_{d-1}.$ So Theorem 3.3 is false if $G(M)$ is Cohen
Macaulay.

  3. (3)

Let $A=k[[x,y]]$, $I=(x^{3},x^{2}y,y^{4})$ and $M=A/I$. So $R=G(A)=k[X,Y]$ and
$G(M)=R/(X^{3},X^{2}Y,Y^{4}).$ Clearly $M$ and $G(M)$ is Cohen Macaulay
because they are of dimension zero. Graded resolution of $G(M)$ is

$0\to R(-4)\oplus R(-6)\to R^{2}(-3)\oplus R(-4)\to R\to 0$

and it is quasi pure resolution. So there exist Cohen Macaulay $A$-modules
with quasi-pure resolution.

  4. (4)

Let $A=k[[x,y]]$, $I=(x^{2},xy,y^{5})$ and $M=A/I$. So $R=G(A)=k[X,Y]$ and
$G(M)=R/(X^{2},XY,Y^{5}).$ Clearly $M$ and $G(M)$ is Cohen Macaulay because
they are of dimension zero. Graded resolution of $G(M)$ is

$0\to R(-3)\oplus R(-6)\to R^{2}(-2)\oplus R(-5)\to R\to 0$

and it is not a quasi pure resolution. This shows there exists $M$ Cohen
Macaulay with $G(M)$ not having a quasi-pure resolution.

##  4\. Hilbert coefficient of the modules of finite projective dimension

In [[3], Theorem 1.1] it first shows that if $(A,\mathfrak{m})$ is a non-
regular Gorenstein local ring and $G(A)$ is Cohen Macaulay, then for all
finite length $A$-modules $E$ of finite projective dimension
$\ell\ell(E)\geq\operatorname{reg}(G(A))+1$ (here $\ell\ell(E)$ denotes the
Lowey length of $E$. Set $c=\operatorname{reg}(G(A))$. In this section, we
first prove if $M$ is Cohen Macaulay of positive dimension with finite
projective dimension then $e_{0}(M)\geq\mu(M)+reg(G(A))$ and
$e_{1}(M)\geq\binom{c+1}{2}$. Then we will show $G(M)$ is Cohen Macaulay if
equality holds for $e_{1}(M)$(see 4.3).

######  4.1.

Recall the Lowey length of a finite length $A$-module $E$ is defined to be the
number

$\ell\ell(E)=\operatorname{min}\\{i\,|\,\mathfrak{m}^{i}E=0\\}.$

Let $G(A)_{+}$ be the irrelevant maximal ideal of $G(A)$. Let $H^{i}(G(A))$ be
the $i$-th local cohomology module of $G(A)$ with respect to $G(A)_{+}$. The
Castelnuovo-Mumford regularity of $G(A)$ is

$\operatorname{reg}(G(A))=\operatorname{max}\\{i+j\,|\,H^{i}(G(A))_{j}\neq
0\\}.$

One can easily check that if $x^{*}$ is $G(A)$-regular element of degree $1$
then $\operatorname{reg}(G(A))=\operatorname{reg}(G(A/xA)).$

######  Lemma 4.2.

Let $(A,\mathfrak{m})$ be Gorenstein local ring. Assume $G(A)$ is Cohen
Macaulay. Let $M$ be Cohen Macaulay module of dimension $r$ with finite
projective dimension. Then $e_{0}(M)\geq\mu(M)+c$ and
$e_{1}(M)\geq\binom{c+1}{2},$ where $c=\operatorname{reg}(G(A)).$

###### Proof.

We may assume that the residue field $k$ is infinite. Let $x_{1},\ldots,x_{r}$
be $A\oplus M$-superficial sequence. Set $B=A/(x_{1},\ldots,x_{r})$ and
$N=M/(x_{1},\ldots,x_{r})M(\text{i.e. }\lambda(N)<\infty).$ Let
$\ell\ell(N)=t,$ i.e.
$G(N)=\bigoplus_{i=0}^{t}\mathfrak{m}^{i}N/\mathfrak{m}^{i+1}N.$ Set
$a_{i}=\lambda(\mathfrak{m}^{i}N/\mathfrak{m}^{i+1}N).$ The Hilbert series of
$N$ is $H_{N}(z)=\mu(N)+a_{1}z+\ldots+a_{t-1}z^{t-1}$. So

$\displaystyle
e_{0}(N)=\mu(N)+a_{1}+\ldots+a_{t-1}\geq\mu(N)+t-1\geq\mu(N)+\operatorname{reg}(G(A)).$

We also have

$\displaystyle e_{1}(N)=$ $\displaystyle a_{1}+2a_{2}+\ldots+(t-1)a_{t-1}$
$\displaystyle\geq$ $\displaystyle 1+2+\ldots+(t-1)\geq 1+2+\ldots+c$
$\displaystyle=$ $\displaystyle\binom{c+1}{2}.$

By ([8], Corollary 10) $\mu(M)=\mu(N)$, $e_{0}(M)=e_{0}(N)$ and $e_{1}(M)\geq
e_{1}(N).$ Hence $e_{0}(M)\geq\mu(M)+\operatorname{reg}(G(A))$ and
$e_{1}(M)\geq\binom{c+1}{2}.$ ∎

The next theorem is about what happens if $e_{1}(M)=\binom{c+1}{2}.$

######  Theorem 4.3.

Let $(A,\mathfrak{m})$ be a Gorenstein local ring with $G(A)$ be Cohen
Macaulay. Let $M$ be Cohen Macaulay module of dimension $r$ having finite
projective dimension. If $e_{1}(M)=\binom{c+1}{2}$, then $G(M)$ is Cohen
Macaulay.

###### Proof.

Let $x_{1},\ldots,x_{r}$ be $A\oplus M$-superficial sequence. Set
$N=M/(x_{1},\ldots,x_{r-1})M.$ By ([8], Corollary 10) $e_{1}(M)=e_{1}(N)$ and
$e_{1}(N)\geq e_{1}(N/x_{r}N)$. So by the hypothesis
$\binom{c+1}{2}=e_{1}(N)\geq e_{1}(N/x_{r}N)\geq\binom{c+1}{2}.$ So
$e_{1}(N)=e_{1}(N/x_{r}N)$. By ([8], Corollary 10) $G(N)$ is Cohen Macaulay.
So by Sally descent $G(M)$ is Cohen Macaulay. ∎

##  5\. Cohen Macaulay modules over complete intersection rings

In this section, we will prove an interesting result on Cohen Macaulay modules
over complete intersection ring(see Theorem 5.7) and we will also give an
application of the Corollary 4.2 and Theorem 4.3. For this, we need to recall
the following things.

######  5.1.

Let $A$ be a local ring and $M$ be an $A$-module. Let
$\beta_{i}^{A}(M)=\lambda(\operatorname{Tor}_{i}(M,k))$ be the $i$-th Betti
number of $M$ over $A.$ The complexity of $M$ over $A$ is defined as

$\textrm{cx}_{A}(M)=\inf\left\\{b\in\mathbb{N}\quad\vline\quad{\limsup_{n\to\infty}}\,\,\frac{\beta_{n}^{A}(M)}{n^{b-1}}<\infty\right\\}.$

Note that $M$ has bounded Betti numbers iff $\textrm{cx}_{A}(M)\leq 1.$

######  5.2.

Let $Q$ be a local ring and $\textbf{f}=f_{1},\ldots,f_{c}$ be a $Q$-regular
sequence. Set $A=Q/(\textbf{f}).$ The Eisenbud operators(see [4]) are
constructed as follows

Let $\mathbb{F}:\cdots
F_{i+2}\xrightarrow{\partial}F_{i+1}\xrightarrow{\partial}F_{i}\ldots$ be a
complex of free $A$-modules.
(a) Choose a sequence of free $Q$-modules $\widetilde{\mathbb{F}_{i}}$ and
maps $\widetilde{\partial}$ between them

$\widetilde{\mathbb{F}}:\cdots\widetilde{F}_{i+2}\xrightarrow{\widetilde{\partial}}\widetilde{F}_{i+1}\xrightarrow{\widetilde{\partial}}\widetilde{F}_{i}\ldots$

such that $\mathbb{F}=\widetilde{\mathbb{F}}\otimes A$.
(b) Since $\widetilde{\partial}^{2}\equiv 0$ modulo$(f_{1},\ldots,f_{c}),$ we
may write $\widetilde{\partial}^{2}=\sum_{j=1}^{c}f_{j}\widetilde{t_{j}}$
where $\widetilde{t_{j}}:\widetilde{F_{i}}\to\widetilde{F}_{i-2}$ are linear
maps for all $i.$
(c) Define, for $j=1,\ldots,c$ the map $t_{j}=t_{j}(Q,\textbf{f},\mathbb{F})$
by $t_{j}=\widetilde{t_{j}}\otimes A.$

The operators $t_{1},\ldots,t_{c}$ are called Eisenbud operators associated to
$\textbf{f}.$ It can be shown that

  1. (1)

$t_{i}$ are uniquely determined up to homotopy.

  2. (2)

$t_{i},t_{j}$ commutes up to homotopy.

######  5.3.

Let $\textbf{g}=g_{1},\ldots,g_{c}$ be another $Q$-regular sequence such that
$(\textbf{g})=(\textbf{f})$. The Eisenbud operators associated to g can be
constructed by using Eisenbud operators associated to f as follows:

Let $f_{i}=\sum_{j=1}^{c}a_{ij}g_{j}\text{ for }i=1,\ldots,c$. Then we can
choose $t_{i}^{\prime}=\sum_{j=1}^{c}a_{ji}t_{c}\text{ for }i=1,\ldots,c$ as
Eisenbud operators for $g_{1},\ldots,g_{c}.$ Note that in [4] there is an
indexing error.

######  5.4.

Let $R=A[t_{1},\ldots,t_{c}]$ be a polynomial ring over $A$ with variable
$t_{1},\ldots,t_{c}$ of degree $2.$ Let $M$ be an $A$-module and let
$\mathbb{F}$ be a free resolution of $M$. So we get well defined maps

$t_{j}:\operatorname{Ext}_{A}^{n}(M,k)\to\operatorname{Ext}_{A}^{n+2}(M,k)\text{
for all }1\leq j\leq c\text{ and all }n.$

This turns $\operatorname{Ext}_{A}^{*}(M,k)=\bigoplus_{i\geq
0}\operatorname{Ext}_{A}^{i}(M,k)$ into a $R$-module. Where $k$ is residue
field of $A.$

Since $\mathfrak{m}\subseteq\text{ann}(\operatorname{Ext}_{A}^{i}(M,k))$ for
all $i\geq 0$ we get that $\operatorname{Ext}_{A}^{*}(M,k)$ is a
$S=R/\mathfrak{m}R=k[t_{1},\ldots,t_{c}]$-module.

######  Remark 5.5.

The subring $k[t_{1},\ldots,t_{r}]$$(r<c)$ of $S$ can be identified with the
ring $S^{\prime}$ of cohomological operators of a presentation
$A=P/(f_{1},\ldots,f_{r})$, where $P=Q/(f_{r+1},\ldots,f_{c}).$

######  5.6.

In ([6], 3.1) Gulliksen proved that if $\text{projdim}_{Q}(M)$ is finite then
$\operatorname{Ext}_{A}^{*}(M,N)$ is finitely generated $R$-module for all
$A$-modules $N$. In ([2], 3.10) Avramov proved a converse for $N=k.$ Note that
if $\text{projdim}_{Q}(M)$ is finite then $\operatorname{Ext}_{A}^{*}(M,k)$ is
finitely generated graded $S$-module of Krull dimension $\textrm{cx}_{A}(M).$

Let $(A,\mathfrak{m})$ be a local ring. For
$x\in\mathfrak{m}^{i}\setminus\mathfrak{m}^{i+1}$ we set $\text{ord}(x)=i$ as
order of $x.$

######  Theorem 5.7.

Let $(Q,\mathfrak{n})$ be a regular local ring with infinite residue field,
$f_{1},\ldots,f_{c}\in\mathfrak{n}^{2}$ of order $s$ such that
$f_{1}^{*},\ldots,f_{c}^{*}$ is a $G(Q)$-regular sequence. Let
$A=Q/(f_{1},\ldots,f_{c})$ and $M$ be Cohen Macaulay $A$-module with
$\operatorname{cx}_{A}(M)=r<c$. Then $M$ has finite projective dimension as
$Q/(g_{r+1},\ldots,g_{c})$-module, for some $g_{r+1},\ldots,g_{c}$. Here
$g_{r+1}^{*},\ldots,g_{c}^{*}$ is a $G(Q)$-regular sequence and
$\operatorname{ord}(g_{i})=s.$

###### Proof.

By 5.6, $\operatorname{Ext}_{A}^{*}(M,k)$ is finitely generated graded
$S$-module of Krull dimension $\textrm{cx}_{A}(M).$ Set
$E=\operatorname{Ext}_{A}^{*}(M,k)$. Let $\xi_{1},\ldots,\xi_{r}\in S_{2}$ be
a system of parameters of $E$ and
$\xi_{i}=\sum_{j=1}^{c}\overline{\beta_{ij}}t_{j}.$ Set
$\beta=(\overline{\beta_{ij}})_{r\times c}$. Since $\xi_{1},\ldots,\xi_{r}\in
S_{2}$ is a system of parameters, the rank of matrix $\beta$ is equals to $r.$

Note that the first $r$ columns of $\beta$ may not be linearly independent.
But we can rearrange the columns of $\beta$ so that the first $r$ columns are
linearly independent. Without loss of generality, we can reorder
$f_{1},\ldots,f_{c}$ so that the first $r$ column of $\beta$ is linearly
independent(see 5.3). Now set $\alpha=(a_{ij})_{c\times c}$, where

$a_{ij}=\left\\{\begin{array}[]{ll}\beta_{ij}&1\leq i\leq r,\,1\leq j\leq c\\\
1&\text{if }i=j\text{ and }i>r\\\ 0&\text{otherwise}\\\ \end{array}\right.$

(here we assume the image of $\beta_{ij}$ in $k$ is $\overline{\beta_{ij}}$.)
Clearly, the matrix $\alpha$ is nonsingular(as $\overline{\alpha}$ is non-
singular). Set $\xi_{j}=t_{j}$ for $j>r.$ Then $S=k[\xi_{1},\ldots,\xi_{c}].$
By ([10], 1.9) there is a regular sequence $\textbf{g}=g_{1},\ldots,g_{c}$
such that $(\textbf{g})=(\textbf{f})$ and if $t_{i}^{\prime}$ are the Eisenbud
operators associated to g, then the action of $t_{j}^{\prime}$ on $E$ is same
as that of $\xi_{j}$ for $j=1,\ldots,c$.

By ([10], 1.9), $[\textbf{g}]=(\alpha^{tr})^{-1}[\textbf{f}]$, where
$\alpha^{tr}$ is the transpose of $\alpha$. We note that
$\operatorname{ord}(g_{i})\geq s$ for all $i$. As $(\textbf{g})=(\textbf{f})$
we get $A=Q/(g_{1},\ldots,g_{c})$. We have $e(A)=s^{c}$. So by [12, 1.8] it
follows that $\operatorname{ord}(g_{i})=s$ for all $i$ and
$g_{1}^{*},\ldots,g_{c}^{*}$ is a $G(Q)$-regular sequence. We also have
$G(A)=G(Q)/(g_{1}^{*},\ldots,g_{c}^{*})$.

The subring $k[\xi_{1},\ldots,\xi_{r}]$ of $S$ can be identified by the ring
$S^{\prime}$ of cohomological operators of a presentation
$A=P/(g_{1},\ldots,g_{r})$, where $P=Q/(g_{r+1},\ldots,g_{c})$. Since
$\operatorname{Ext}_{A}^{*}(M,k)$ is finitely generated graded
$S^{\prime}$-module, we obtained by 5.6 that $\text{projdim}_{P}(M)$ is
finite. This proves our result. ∎

As a consequence, we obtain:

######  Theorem 5.8.

Let $(Q,\mathfrak{n})$ be a regular local ring with infinite residue field,
$f_{1},\ldots,f_{c}\in\mathfrak{n}^{2}$ of order $s$ such that
$f_{1}^{*},\ldots,f_{c}^{*}$ is a $G(Q)$-regular sequence. Let
$A=Q/(f_{1},\ldots,f_{c})$ and $M$ be Cohen Macaulay $A$-module with
$\operatorname{cx}_{A}(M)=r<c$. Then $e_{0}(M)\geq\mu(M)+\alpha$ and
$e_{1}(M)\geq\binom{\alpha+1}{2}$, where $\alpha=(c-r)(s-1).$ Moreover if
$e_{1}(M)=\binom{\alpha+1}{2}$ then $G(M)$ is Cohen Macaulay.

###### Proof.

We may assume that $A$ has an infinite residue field(see [10], 1.1). By
Theorem 5.7, we get that $A=B/(g_{1},\ldots,g_{r})$ and $M$ has finite
projective dimension as $B$-module, where $B=Q/(g_{r+1},\ldots,g_{c})$ and
$(g_{1}^{*},\ldots,g_{c}^{*})$ is a $G(Q)$-regular sequence. Since
$\text{ord}(g_{i})=s$ for all $1\leq i\leq c$, we obtain that
$\operatorname{reg}(G(B))=(c-r)(s-1)$. Set $\alpha=(c-r)(s-1).$ By Lemma 4.2,
$e_{0}(M)\geq\mu(M)+\alpha$ and $e_{1}(M)\geq\binom{\alpha+1}{2}.$ By Theorem
4.3 if $e_{1}(M)=\binom{\alpha+1}{2}$, then $G(M)$ is Cohen Macaulay
$G(B)$-module (and so a Cohen-Macaulay $G(A)$-module). ∎

## References

  * [1] H. Ananthnarayan, Manav Batavia, and Omkar Javadekar, _When do associated graded modules have pure resolutions?_ , arXiv preprint arXiv:2308.00654 (2023).
  * [2] Luchezar L. Avramov, _Modules of finite virtual projective dimension_ , Inventiones mathematicae 96 (1989), no. 1, 71–101.
  * [3] Luchezar L. Avramov, Ragnar-Olaf Buchweitz, Srikanth B. Iyengar, and Claudia Miller, _Homology of perfect complexes_ , Advances in Mathematics 223 (2010), no. 5, 1731–1781.
  * [4] David Eisenbud, _Homological algebra on a complete intersection, with an application to group representations_ , Transactions of the American Mathematical Society 260 (1980), no. 1, 35–64.
  * [5] Gert-Martin Greuel, Gerhard Pfister, and Hans Schönemann, _Singular—a computer algebra system for polynomial computations_ , Symbolic computation and automated reasoning, AK Peters/CRC Press, 2001, pp. 227–233.
  * [6] Tor H. Gulliksen, _A change of ring theorem with applications to poincaré series and intersection multiplicity_ , Mathematica Scandinavica 34 (1974), no. 2, 167–183.
  * [7] Hideyuki Matsumura, _Commutative ring theory_ , no. 8, Cambridge university press, 1989.
  * [8] Tony J. Puthenpurakal, _Hilbert coefficients of a Cohen–Macaulay module_ , Journal of Algebra 264 (2003), no. 1, 82–97.
  * [9] by same author, _Ratliff–Rush filtration, regularity and depth of higher associated graded modules: Part I_ , Journal of Pure and Applied Algebra 208 (2007), no. 1, 159–176.
  * [10] by same author, _The Hilbert function of a maximal Cohen–Macaulay module. Part II_ , Journal of Pure and Applied Algebra 218 (2014), no. 12, 2218–2225.
  * [11] by same author, _On associated graded modules having a pure resolution_ , Proceedings of the American Mathematical Society 144 (2016), no. 10, 4107–4114.
  * [12] M. E. Rossi and G. Valla, _Multiplicity and $t$-isomultiple ideals_, Nagoya Math. J. 110 (1988), 81–111.