PMID- 36502252
OWN - NLM
STAT- PubMed-not-MEDLINE
DCOM- 20221216
LR  - 20221221
IS  - 1424-8220 (Electronic)
IS  - 1424-8220 (Linking)
VI  - 22
IP  - 23
DP  - 2022 Dec 6
TI  - Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata 
      with Digital Clocks.
LID - 10.3390/s22239552 [doi]
LID - 9552
AB  - Metric temporal logic (MTL) is a popular real-time extension of linear temporal 
      logic (LTL). This paper presents a new simple SAT-based bounded model-checking 
      (SAT-BMC) method for MTL interpreted over discrete infinite timed models 
      generated by discrete timed automata with digital clocks. We show a new 
      translation of the existential part of MTL to the existential part of linear 
      temporal logic with a new set of atomic propositions and present the details of 
      the new translation. We compare the new method's advantages to the old method 
      based on a translation of the hard reset LTL (HLTL). Our method does not need new 
      clocks or new transitions. It uses only one path and requires a smaller number of 
      propositional variables and clauses than the HLTL-based method. We also 
      implemented the new method, and as a case study, we applied the technique to 
      analyze several systems. We support the theoretical description with the 
      experimental results demonstrating the method's efficiency.
FAU - Zbrzezny, Agnieszka M
AU  - Zbrzezny AM
AUID- ORCID: 0000-0001-9897-3561
AD  - Faculty of Mathematics and Computer Science, University of Warmia and Mazury, 
      Sloneczna 54, 10-710 Olsztyn, Poland.
FAU - Zbrzezny, Andrzej
AU  - Zbrzezny A
AUID- ORCID: 0000-0003-2771-9683
AD  - Department of Mathematics and Computer Science, Jan Dlugosz University in 
      Czestochowa, Armii Krajowej 13/15, 42-200 Czestochowa, Poland.
LA  - eng
PT  - Journal Article
DEP - 20221206
PL  - Switzerland
TA  - Sensors (Basel)
JT  - Sensors (Basel, Switzerland)
JID - 101204366
SB  - IM
PMC - PMC9737090
OTO - NOTNLM
OT  - bounded model checking
OT  - digital clocks
OT  - metric temporal logic
OT  - satisfiability problem
OT  - timed automata
COIS- The authors declare no conflict of interest.
EDAT- 2022/12/12 06:00
MHDA- 2022/12/12 06:01
PMCR- 2022/12/06
CRDT- 2022/12/11 01:39
PHST- 2022/11/03 00:00 [received]
PHST- 2022/11/30 00:00 [revised]
PHST- 2022/12/02 00:00 [accepted]
PHST- 2022/12/11 01:39 [entrez]
PHST- 2022/12/12 06:00 [pubmed]
PHST- 2022/12/12 06:01 [medline]
PHST- 2022/12/06 00:00 [pmc-release]
AID - s22239552 [pii]
AID - sensors-22-09552 [pii]
AID - 10.3390/s22239552 [doi]
PST - epublish
SO  - Sensors (Basel). 2022 Dec 6;22(23):9552. doi: 10.3390/s22239552.